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

Theorem lebi 145
Description: L.e. to biconditional.
Hypotheses
Ref Expression
lebi.1 ab
lebi.2 ba
Assertion
Ref Expression
lebi a = b

Proof of Theorem lebi
StepHypRef Expression
1 lebi.2 . . . . 5 ba
21df-le2 131 . . . 4 (ba) = a
32ax-r1 35 . . 3 a = (ba)
4 ax-a2 31 . . 3 (ba) = (ab)
53, 4ax-r2 36 . 2 a = (ab)
6 lebi.1 . . 3 ab
76df-le2 131 . 2 (ab) = b
85, 7ax-r2 36 1 a = b
Colors of variables: term
Syntax hints:   = wb 1  wle 2  wo 6
This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36
This theorem depends on definitions:  df-le2 131
This theorem is referenced by:  distlem  188  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  wlem1  243  mccune2  247  wql1lem  287  wql2lem  288  womle2a  295  nom14  311  go1  343  k1-8a  355  2vwomlem  365  wr5-2v  366  wdf-c2  384  ska2  432  ska4  433  ka4ot  435  ortha  438  cmtr1com  493  i3or  497  i3ri3  538  i3li3  539  i32i3  540  ud4lem1a  577  i2bi  722  u12lem  771  u3lemax4  796  u3lemax5  797  bi1o1a  798  biao  799  i2i1i1  800  3vth2  805  3vded11  814  3vded12  815  1oaiii  823  3vroa  831  negant  852  negant3  860  negant4  862  neg3ant1  866  mhlem  876  mh  879  distid  887  oago3.21x  890  cancel  892  gomaex4  900  gomaex3lem2  915  oau  929  oa23  936  oaliii  1001  oagen1  1014  oadist  1019  oadistb  1020  oadistc0  1021  oadistc  1022  oadistd  1023  4oaiii  1040  4oagen1  1042  4oadist  1044  lem3.3.5lem  1054  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem4.6.6i0j1  1086  lem4.6.6i0j2  1087  lem4.6.6i0j3  1088  lem4.6.6i0j4  1089  lem4.6.6i2j1  1094  lem4.6.6i2j4  1095  lem4.6.6i3j0  1096  lem4.6.6i3j1  1097  lem4.6.6i4j2  1099  com3iia  1100  lem4.6.7  1101  wdwom  1104  ml  1121  mldual2i  1125  ml3  1128  vneulem1  1129  vneulem6  1134  vneulem7  1135  vneulem13  1141  vneulemexp  1146
  Copyright terms: Public domain W3C validator