QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  lecom GIF version

Theorem lecom 180
Description: Comparable elements commute. Beran 84 2.3(iii) p. 40. (Contributed by NM, 30-Aug-1997.)
Hypothesis
Ref Expression
lecom.1 ab
Assertion
Ref Expression
lecom a C b

Proof of Theorem lecom
StepHypRef Expression
1 orabs 120 . . . 4 (a ∪ (ab )) = a
21ax-r1 35 . . 3 a = (a ∪ (ab ))
3 lecom.1 . . . . . 6 ab
43df2le2 136 . . . . 5 (ab) = a
54ax-r1 35 . . . 4 a = (ab)
65ax-r5 38 . . 3 (a ∪ (ab )) = ((ab) ∪ (ab ))
72, 6ax-r2 36 . 2 a = ((ab) ∪ (ab ))
87df-c1 132 1 a C b
Colors of variables: term
Syntax hints:  wle 2   C wc 3   wn 4  wo 6  wa 7
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-le2 131  df-c1 132
This theorem is referenced by:  comorr  184  coman1  185  gsth  489  gt1  492  i3bi  496  oi3ai3  503  lem4  511  u1lemc6  706  comi12  707  u1lemle1  710  u2lemle1  711  u3lemle1  712  u4lemle1  713  u5lemle1  714  u12lembi  726  u3lem15  795  bi1o1a  798  3vcom  813  3vded21  817  1oa  820  2oalem1  825  mlalem  832  bi3  839  bi4  840  orbi  842  negantlem1  848  elimconslem  867  elimcons  868  comanblem1  870  mhlemlem1  874  mhlem  876  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  e2ast2  894  e2astlem1  895  govar  896  gomaex3lem1  914  gomaex3lem2  915  oa3to4lem1  945  oa3to4lem2  946  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oacom2  1012  oa3moa3  1029  lem4.6.2e1  1082  lem4.6.6i1j3  1094  lem4.6.7  1103
  Copyright terms: Public domain W3C validator