Theorem coman2 186

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

Assertion

Ref	Expression
coman2	(a ∩ b) C b

Proof of Theorem coman2

Step	Hyp	Ref	Expression
1		ancom 74	. 2 (a ∩ b) = (b ∩ a)
2		coman1 185	. 2 (b ∩ a) C b
3	1, 2	bctr 181	1 (a ∩ b) C b

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  df-c2 133

This theorem is referenced by:  comanr2  465  gsth  489  dfi3b  499  i3con  551  ud1lem1  560  ud2lem3  565  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  u2lemle2  716  u1lembi  720  u2lembi  721  u1lem4  757  u4lem6  768  u1lem8  776  u3lem11  786  u3lem13b  790  1oa  820  mlalem  832  bi3  839  mlaconj4  844  neg3antlem2  865  comanblem1  870  cancellem  891  govar  896  lem4.6.2e1  1082