Theorem comorr 184

Description: Commutation law. Does not use OML.

Assertion

Ref	Expression
comorr	a C (a ∪ b)

Proof of Theorem comorr

Step	Hyp	Ref	Expression
1		leo 158	. 2 a ≤ (a ∪ b)
2	1	lecom 180	1 a C (a ∪ b)

Syntax hints:   C wc 3   ∪ wo 6

This theorem is referenced by:  comid 187  comor1 461  nbdi 486  df2i3 498  i3lem1 504  i3con 551  ud1lem1 560  ud1lem3 562  ud3lem1c 568  ud3lem2 571  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud4lem2 582  ud5lem3b 592  ud5lem3 594  u3lemaa 602  u3lemana 607  u4lem1 737  u3lem10 785  u3lem13a 789  u3lem13b 790  i1abs 801  3vth5 808  mhlem1 877  marsdenlem1 880  marsdenlem2 881  oau 929  oa23 936  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

Copyright terms: Public domain