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

Theorem bile 142
 Description: Biconditional to l.e.
Hypothesis
Ref Expression
bile.1 a = b
Assertion
Ref Expression
bile ab

Proof of Theorem bile
StepHypRef Expression
1 bile.1 . . . 4 a = b
21ax-r5 38 . . 3 (ab) = (bb)
3 oridm 110 . . 3 (bb) = b
42, 3ax-r2 36 . 2 (ab) = b
54df-le1 130 1 ab
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2   ∪ wo 6 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-t 41  df-f 42  df-le1 130 This theorem is referenced by:  qlhoml1a  143  qlhoml1b  144  leid  148  str  189  mccune2  247  wom3  367  i3ri3  538  i3li3  539  i32i3  540  u12lem  771  sadm3  838  mlaconj4  844  mlaconjo  886  oaidlem2  931  oaidlem2g  932  distoah1  940  d3oa  995  oadist2  1009  mloa  1018  oadist  1019  dp15lemf  1157  dp35leme  1171  dp35lemd  1172  xdp15  1197  xxdp15  1200  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
 Copyright terms: Public domain W3C validator