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

Theorem lecon 154
 Description: Contrapositive for l.e. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
le.1 ab
Assertion
Ref Expression
lecon ba

Proof of Theorem lecon
StepHypRef Expression
1 ax-a2 31 . . . 4 (ba) = (ab)
2 oran 87 . . . 4 (ba) = (ba )
3 le.1 . . . . 5 ab
43df-le2 131 . . . 4 (ab) = b
51, 2, 43tr2 64 . . 3 (ba ) = b
65con3 68 . 2 (ba ) = b
76df2le1 135 1 ba
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ 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-le1 130  df-le2 131 This theorem is referenced by:  lecon1  155  lecon3  157  lei3  246  nom14  311  i2or  344  ska4  433  binr1  517  ud4lem1a  577  biao  799  3vded12  815  3vded22  818  3vroa  831  sa5  836  elimconslem  867  comanb  872  marsdenlem3  882  gomaex3h4  905  gomaex3h7  908  gomaex3h11  912  oa3to4lem6  950  oa6todual  952  oa6fromdual  953  oa4to6  965  oa8todual  971  lem3.3.7i4e1  1069  lem3.3.7i5e1  1072
 Copyright terms: Public domain W3C validator