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

Theorem necon3bi 2562
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 2525 . . 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 1642    =/= wne 2521
This theorem is referenced by:  r19.2zb  3620  pwne  4256  onnev  4849  alephord  7789  ackbij1lem18  7950  fin23lem26  8038  fin1a2lem6  8118  alephom  8294  gchxpidm  8378  egt2lt3  12575  alexsubALTlem2  17838  alexsubALTlem4  17840  ptcmplem2  17843  nmoid  18347  logccne0ALT  23662  esumcst  23721  hasheuni  23741  axlowdimlem17  25145  limsucncmpi  25443  ovoliunnfl  25488  voliunnfl  25490  volsupnfl  25491  dvreasin  25515  pellexlem5  26241  2trllem1  27713  2pthon  27721  2pthon3v  27723  frgrancvvdeqlem3  27848  frgrancvvdeqlem9  27857  lsat0cv  29275
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 2523
  Copyright terms: Public domain W3C validator