MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3bi Unicode version

Theorem necon3bi 2616
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon3bi.1  |-  ( A  =  B  ->  ph )
Assertion
Ref Expression
necon3bi  |-  ( -. 
ph  ->  A  =/=  B
)

Proof of Theorem necon3bi
StepHypRef Expression
1 nne 2579 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bi.1 . . 3  |-  ( A  =  B  ->  ph )
31, 2sylbi 188 . 2  |-  ( -.  A  =/=  B  ->  ph )
43con1i 123 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2575
This theorem is referenced by:  r19.2zb  3686  pwne  4334  onnev  4925  alephord  7920  ackbij1lem18  8081  fin23lem26  8169  fin1a2lem6  8249  alephom  8424  gchxpidm  8508  egt2lt3  12768  alexsubALTlem2  18040  alexsubALTlem4  18042  ptcmplem2  18045  nmoid  18737  2trllemA  21511  2pthon  21563  2pthon3v  21565  logccne0OLD  24356  hasheuni  24436  axlowdimlem17  25809  limsucncmpi  26107  ovoliunnfl  26155  voliunnfl  26157  volsupnfl  26158  dvreasin  26187  pellexlem5  26794  frgrancvvdeqlem3  28143  frgrancvvdeqlem9  28152  lsat0cv  29528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2577
  Copyright terms: Public domain W3C validator