Theorem comor1 461

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

Assertion

Ref	Expression
comor1	(a ∪ b) C a

Proof of Theorem comor1

Step	Hyp	Ref	Expression
1		comorr 184	. 2 a C (a ∪ b)
2	1	comcom 453	1 (a ∪ b) C a

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:  comor2  462  oml6  488  dfi3b  499  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem2  561  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  u1lem8  776  u1lem11  780  u3lem11  786  u3lem15  795  bi1o1a  798  test  802  test2  803  neg3antlem2  865  elimconslem  867  elimcons  868  mhlemlem1  874  mhlem  876  mlaconjolem  885