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

Theorem necon3bi 2487
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 2450 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon3bi.1 . . 3  |-  ( A  =  B  ->  ph )
31, 2sylbi 187 . 2  |-  ( -.  A  =/=  B  ->  ph )
43con1i 121 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  r19.2zb  3544  pwne  4177  onnev  4770  alephord  7702  ackbij1lem18  7863  fin23lem26  7951  fin1a2lem6  8031  alephom  8207  gchxpidm  8291  egt2lt3  12484  alexsubALTlem2  17742  alexsubALTlem4  17744  ptcmplem2  17747  nmoid  18251  logccne0ALT  23398  esumcst  23436  hasheuni  23453  axlowdimlem17  24586  limsucncmpi  24884  dvreasin  24923  pellexlem5  26918  lsat0cv  29223
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator