Theorem comor1 443

Description: Commutation law.

Assertion

Ref	Expression
comor1	(a ∪ b) C a

Proof of Theorem comor1

Step	Hyp	Ref	Expression
1		comorr 176	. 2 a C (a ∪ b)
2	1	comcom 435	1 (a ∪ b) C a

Syntax hints:   C wc 3   ∪ wo 6

This theorem is referenced by:  comor2 444  oml6 470  dfi3b 481  i3con 533  i3orlem7 540  i3orlem8 541  ud1lem2 543  ud1lem3 544  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem3d 557  ud3lem3 558  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem3b 566  ud4lem3 567  ud5lem1 571  ud5lem3 576  u4lemana 590  u4lemoa 605  u4lemona 610  u3lemob 614  u3lemonb 619  u4lemle2 700  u4lem1 719  u4lem5 746  u4lem6 750  u1lem8 758  u1lem11 762  u3lem11 768  u3lem15 777  bi1o1a 780  test 784  test2 785  neg3antlem2 847  elimconslem 849  elimcons 850  mhlemlem1 856  mhlem 858  mlaconjolem 867

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org