Theorem coman1 185

Description: Commutation law. Does not use OML. (Contributed by NM, 30-Aug-1997.)

Assertion

Ref	Expression
coman1	(a ∩ b) C a

Proof of Theorem coman1

Step	Hyp	Ref	Expression
1		lea 160	. 2 (a ∩ b) ≤ a
2	1	lecom 180	1 (a ∩ b) C a

Syntax hints:   C wc 3   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131  df-c1 132

This theorem is referenced by:  coman2  186  comanr1  464  oml4  487  gsth2  490  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  i3lem1  504  comi31  508  i3con  551  ud1lem1  560  ud3lem1a  566  ud3lem1c  568  ud3lem1  570  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem3a  591  ud5lem3  594  u2lemaa  601  u2lemana  606  u1lemab  610  u3lemab  612  u1lemanb  615  u3lemanb  617  u1lemle2  715  u2lemle2  716  u1lembi  720  u2lembi  721  u1lem4  757  u4lem6  768  u1lem8  776  u3lem11  786  u3lem13b  790  test  802  1oa  820  2oath1  826  oale  829  mlalem  832  bi3  839  mlaconj4  844  neg3antlem2  865  comanblem1  870  cancellem  891  govar  896  gomaex3lem3  916  lem4.6.2e1  1082