Theorem coman2 186

Description: Commutation law. Does not use OML.

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 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 1079

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

Copyright terms: Public domain