Theorem ancom 68

Description: Commutative law.

Assertion

Ref	Expression
ancom	(a ^ b) = (b ^ a)

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		ax-a2 30	. . 3 (a_|_ v b_|_) = (b_|_ v a_|_)
2	1	ax-r4 36	. 2 (a_|_ v b_|_)_|_ = (b_|_ v a_|_)_|_
3		df-a 39	. 2 (a ^ b) = (a_|_ v b_|_)_|_
4		df-a 39	. 2 (b ^ a) = (b_|_ v a_|_)_|_
5	2, 3, 4	3tr1 60	1 (a ^ b) = (b ^ a)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  ran 71  an12 74  an32 76  dfnb 87  bicom 88  dff 93  an1r 99  an0r 101  1b 109  leao 116  mi 117  di 118  omlem1 119  lear 153  lelan 159  ledi 166  ledir 167  comm1 171  coman2 178  cmtrcom 182  wancom 195  wwoml3 205  wwfh1 208  wwfh2 209  ska5 225  ska8 228  ska13 233  wlem1 235  lei3 238  i3id 243  i1i2 258  i3i4 262  i5con 264  1i1 266  wql2lem3 282  wql2lem5 284  nomb41 291  nomb32 292  nomcon1 294  nomcon2 295  nom21 306  nom22 307  nom30 311  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  nom60 329  2vwomr2 344  2vwomlem 347  wlan 352  wom5 363  wcomlem 364  wdf-c2 366  wle2an 386  wledi 387  wcom3i 404  wfh1 405  wfh2 406  wcom2or 409  ska2 414  ska4 415  woml6 418  woml7 419  oml5 431  oml3 434  comcom 435  com3i 449  fh1 451  fh2 452  fh1r 455  fh2r 456  fh4c 460  fh3rc 463  fh4rc 464  com2or 465  oml4 469  gsth 471  gsth2 472  i3bi 478  df2i3 480  dfi3b 481  oi3ai3 485  i3lem3 488  lem4 493  i3le 497  i3abs3 506  i3ancom 508  i3lan 518  i3th1 525  i3con 533  i3orlem8 541  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem1 545  ud2lem3 547  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem2 553  ud3lem3c 556  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  ud5lem3 576  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u1lemana 587  u2lemana 588  u3lemana 589  u4lemana 590  u5lemana 591  u2lemab 593  u3lemab 594  u3lemanb 599  u4lemoa 605  u3lemob 614  u3lemonb 619  u1lemc4 683  u3lemc4 685  u4lemc4 686  u5lemc4 687  i1com 690  comi1 691  u2lemle2 698  u4lemle2 700  u5lemle2 701  u1lembi 702  u2lembi 703  u5lembi 707  u12lembi 708  u21lembi 709  u4lem1 719  u3lem1n 723  u4lem1n 724  u5lem1n 725  u1lem3 731  u3lem3 733  u4lem3 734  u5lem3 735  u1lem4 739  u4lem4 741  u1lem5 743  u2lem5 744  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u24lem 752  u1lem7 754  u2lem7 755  u3lem10 767  u3lem11 768  u3lem11a 769  u3lem13a 771  u3lem13b 772  u3lem14a 773  u3lemax4 778  bi1o1a 780  test 784  3vth1 786  3vth5 790  3vth9 794  3vded11 796  3vded21 799  3vded3 801  1oaiii 805  1oaii 806  3vroa 813  mlaoml 815  sa5 818  salem1 819  bi3 821  bi4 822  imp3 823  orbi 824  mlaconj4 826  mlaconj 827  negantlem2 831  negantlem10 843  comanblem1 852  mhlemlem1 856  mhlem 858  mhlem1 859  marsdenlem1 862  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mhcor1 870  cancellem 873  kb10iii 875  go2n4 879  gomaex4 880  go2n6 881  gomaex3lem1 894  gomaex3lem7 900  gomaex3lem9 902  oas 905  oau 909  oaur 910  oa4v3v 914  oal42 915  oa23 916  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem5 929  oa6to4 938  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4dcom 950  oa8to5 952  oa4uto4g 955  oa4gto4u 956  oa3-1lem 962  oa3-5lem 964  oa3-u1lem 965  oa3-u2lem 966  oa3-6to3 967  oa3-2to2s 970  oa3-u1 971  oa3-u2 972  oa3-1to5 973  d4oa 976  oaliii 981  oalii 982  oaliv 983  oalem1 985  oalem2 986  oacom 991  oacom3 993  oadistc0 1001  oadistc 1002  4oaiii 1019

This theorem was proved from axioms:  ax-a2 30  ax-r1 34  ax-r2 35  ax-r4 36

This theorem depends on definitions:  df-a 39

metamath.org