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

Theorem necon3bi 2647
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 2607 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bi.1 . . 3  |-  ( A  =  B  ->  ph )
31, 2sylbi 189 . 2  |-  ( -.  A  =/=  B  ->  ph )
43con1i 124 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  r19.2zb  3720  pwne  4369  onnev  4961  alephord  7961  ackbij1lem18  8122  fin23lem26  8210  fin1a2lem6  8290  alephom  8465  gchxpidm  8549  egt2lt3  12810  alexsubALTlem2  18084  alexsubALTlem4  18086  ptcmplem2  18089  nmoid  18781  2trllemA  21555  2pthon  21607  2pthon3v  21609  logccne0OLD  24400  hasheuni  24480  axlowdimlem17  25902  limsucncmpi  26200  ovoliunnfl  26259  voliunnfl  26261  volsupnfl  26262  dvreasin  26303  pellexlem5  26909  frgrancvvdeqlem3  28494  frgrancvvdeqlem9  28503  lsat0cv  29904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-ne 2603
  Copyright terms: Public domain W3C validator