Theorem comorr 176

Description: Commutation law. Does not use OML.

Assertion

Ref	Expression
comorr	a C (a v b)

Proof of Theorem comorr

Step	Hyp	Ref	Expression
1		leo 150	. 2 a =< (a v b)
2	1	lecom 172	1 a C (a v b)

Syntax hints:   C wc 3   v wo 6

This theorem is referenced by:  comid 179  comor1 443  nbdi 468  df2i3 480  i3lem1 486  i3con 533  ud1lem1 542  ud1lem3 544  ud3lem1c 550  ud3lem2 553  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud5lem3b 574  ud5lem3 576  u3lemaa 584  u3lemana 589  u4lem1 719  u3lem10 767  u3lem13a 771  u3lem13b 772  i1abs 783  3vth5 790  mhlem1 859  marsdenlem1 862  marsdenlem2 863  oau 909  oa23 916

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

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123  df-c1 124

metamath.org