Theorem ancom 74

Description: Commutative law. (Contributed by NM, 10-Aug-1997.)

Assertion

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

Proof of Theorem ancom

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

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

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

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  1040  lem3.3.3lem2  1050  lem3.3.4  1053  lem3.3.7i0e2  1058  lem3.3.7i1e2  1061  lem3.3.7i3e1  1066  lem3.3.7i5e2  1073  lem3.4.6  1079  lem4.6.2e1  1082  lem4.6.6i2j4  1097  lem4.6.6i4j2  1101  mli  1126  mlduali  1128  vneulem5  1135  vneulem9  1139  vneulem11  1141  vneulem16  1146  vneulemexp  1148  l42modlem1  1149  modexp  1152  dp15lemf  1159  dp53lema  1163  dp53lemb  1164  dp53lemf  1168  dp35leme  1173  dp35lemd  1174  dp35lemb  1176  dp35lem0  1179  dp41lemb  1183  dp41lemc0  1184  dp41lemd  1186  dp41leme  1187  dp41lemf  1188  dp41lemk  1192  dp41leml  1193  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  testmod1  1214  testmod2  1215  testmod2expanded  1216