Theorem comor2 462

Description: Commutation law. (Contributed by NM, 9-Nov-1997.)

Assertion

Ref	Expression
comor2	(a ∪ b) C b

Proof of Theorem comor2

Step	Hyp	Ref	Expression
1		ax-a2 31	. 2 (a ∪ b) = (b ∪ a)
2		comor1 461	. 2 (b ∪ a) C b
3	1, 2	bctr 181	1 (a ∪ b) C b

Syntax hints:   C wc 3   ∪ wo 6

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  comorr2  463  oml6  488  gsth2  490  dfi3b  499  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem3  562  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem3b  584  ud4lem3  585  ud5lem1  589  ud5lem3  594  u4lemana  608  u4lemoa  623  u4lemona  628  u3lemob  632  u3lemonb  637  u4lemle2  718  u4lem1  737  u4lem5  764  u4lem6  768  u1lem11  780  u3lem11  786  u3lem15  795  test  802  test2  803  3vded21  817  neg3antlem2  865  mhlem  876  mhlem1  877