Theorem ancom 74

Description: Commutative law.

Assertion

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

Proof of Theorem ancom

Step	Hyp	Ref	Expression
1		ax-a2 31	. . 3 (a' v b') = (b' v a')
2	1	ax-r4 37	. 2 (a' v b')' = (b' v a')'
3		df-a 40	. 2 (a ^ b) = (a' v b')'
4		df-a 40	. 2 (b ^ a) = (b' v a')'
5	2, 3, 4	3tr1 63	1 (a ^ b) = (b ^ a)

Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  ran 78  an12 81  an32 83  dfnb 95  bicom 96  dff 101  an1r 107  an0r 109  1b 117  leao 124  mi 125  di 126  omlem1 127  lear 161  lelan 167  ledi 174  ledir 175  comm1 179  coman2 186  cmtrcom 190  wancom 203  wwoml3 213  wwfh1 216  wwfh2 217  ska5 233  ska8 236  ska13 241  wlem1 243  lei3 246  i3id 251  i1i2 266  i3i4 270  i5con 272  1i1 274  wql2lem3 290  wql2lem5 292  nomb41 299  nomb32 300  nomcon1 302  nomcon2 303  nom21 314  nom22 315  nom30 319  nom40 325  nom41 326  nom42 327  nom43 328  nom44 329  nom45 330  nom50 331  nom51 332  nom52 333  nom53 334  nom54 335  nom55 336  nom60 337  k1-6 353  k1-7 354  2vwomr2 362  2vwomlem 365  wlan 370  wom5 381  wcomlem 382  wdf-c2 384  wle2an 404  wledi 405  wcom3i 422  wfh1 423  wfh2 424  wcom2or 427  ska2 432  ska4 433  woml6 436  woml7 437  oml5 449  oml3 452  comcom 453  com3i 467  fh1 469  fh2 470  fh1r 473  fh2r 474  fh4c 478  fh3rc 481  fh4rc 482  com2or 483  oml4 487  gsth 489  gsth2 490  i3bi 496  df2i3 498  dfi3b 499  oi3ai3 503  i3lem3 506  lem4 511  i3le 515  i3abs3 524  i3ancom 526  i3lan 536  i3th1 543  i3con 551  i3orlem8 559  ud1lem1 560  ud1lem2 561  ud1lem3 562  ud2lem1 563  ud2lem3 565  ud3lem1a 566  ud3lem1b 567  ud3lem1c 568  ud3lem1d 569  ud3lem2 571  ud3lem3c 574  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud4lem2 582  ud4lem3b 584  ud4lem3 585  ud5lem1a 586  ud5lem1b 587  ud5lem1c 588  ud5lem2 590  ud5lem3a 591  ud5lem3b 592  ud5lem3c 593  ud5lem3 594  u1lemaa 600  u2lemaa 601  u3lemaa 602  u4lemaa 603  u5lemaa 604  u1lemana 605  u2lemana 606  u3lemana 607  u4lemana 608  u5lemana 609  u2lemab 611  u3lemab 612  u3lemanb 617  u4lemoa 623  u3lemob 632  u3lemonb 637  u1lemc4 701  u3lemc4 703  u4lemc4 704  u5lemc4 705  i1com 708  comi1 709  u2lemle2 716  u4lemle2 718  u5lemle2 719  u1lembi 720  u2lembi 721  u5lembi 725  u12lembi 726  u21lembi 727  u4lem1 737  u3lem1n 741  u4lem1n 742  u5lem1n 743  u1lem3 749  u3lem3 751  u4lem3 752  u5lem3 753  u1lem4 757  u4lem4 759  u1lem5 761  u2lem5 762  u4lem5 764  u5lem5 765  u4lem6 768  u5lem6 769  u24lem 770  u1lem7 772  u2lem7 773  u3lem10 785  u3lem11 786  u3lem11a 787  u3lem13a 789  u3lem13b 790  u3lem14a 791  u3lemax4 796  bi1o1a 798  test 802  3vth1 804  3vth5 808  3vth9 812  3vded11 814  3vded21 817  3vded3 819  1oaiii 823  1oaii 824  3vroa 831  mlaoml 833  sa5 836  salem1 837  bi3 839  bi4 840  imp3 841  orbi 842  mlaconj4 844  mlaconj 845  negantlem2 849  negantlem10 861  comanblem1 870  mhlemlem1 874  mhlem 876  mhlem1 877  marsdenlem1 880  marsdenlem2 881  marsdenlem3 882  marsdenlem4 883  mlaconjolem 885  mhcor1 888  cancellem 891  kb10iii 893  e2ast2 894  go2n4 899  gomaex4 900  go2n6 901  gomaex3lem1 914  gomaex3lem7 920  gomaex3lem9 922  oas 925  oau 929  oaur 930  oa4v3v 934  oal42 935  oa23 936  oa3to4lem1 945  oa3to4lem2 946  oa3to4lem5 949  oa6to4 958  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa4dcom 970  oa8to5 972  oa4uto4g 975  oa4gto4u 976  oa3-1lem 982  oa3-5lem 984  oa3-u1lem 985  oa3-u2lem 986  oa3-6to3 987  oa3-2to2s 990  oa3-u1 991  oa3-u2 992  oa3-1to5 993  d4oa 996  oaliii 1001  oalii 1002  oaliv 1003  oalem1 1005  oalem2 1006  oacom 1011  oacom3 1013  oadistc0 1021  oadistc 1022  4oaiii 1039  lem3.3.3lem2 1049  lem3.3.4 1052  lem3.3.7i0e2 1057  lem3.3.7i1e2 1060  lem3.3.7i3e1 1065  lem3.3.7i5e2 1072  lem3.4.6 1078  lem4.6.2e1 1079  lem4.6.6i2j4 1094  lem4.6.6i4j2 1098

This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37

This theorem depends on definitions:  df-a 40

Copyright terms: Public domain