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

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

Proof of Theorem necon3bi
StepHypRef Expression
1 necon3bi.1 . . 3  |-  ( A  =  B  ->  ph )
21con3i 135 . 2  |-  ( -. 
ph  ->  -.  A  =  B )
32neqned 2657 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1398    =/= wne 2649
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 185  df-ne 2651
This theorem is referenced by:  r19.2zb  3907  pwne  4603  pwne0  4607  onnev  5072  alephord  8447  ackbij1lem18  8608  fin23lem26  8696  fin1a2lem6  8776  alephom  8951  gchxpidm  9036  egt2lt3  14021  symgfix2  16640  chfacfisf  19522  chfacfisfcpmat  19523  alexsubALTlem2  20714  alexsubALTlem4  20716  ptcmplem2  20719  nmoid  21415  cxplogb  23325  axlowdimlem17  24463  2trllemA  24754  2pthon  24806  2pthon3v  24808  frgrancvvdeqlem3  25234  frgrancvvdeqlem9  25243  hasheuni  28314  limsucncmpi  30138  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  dvasin  30343  pellexlem5  31008  icccncfext  31929  ioodvbdlimc1lem1  31967  volioc  32010  fourierdlem32  32160  fourierdlem49  32177  fourierdlem73  32201  fourierswlem  32252  fouriersw  32253  lsat0cv  35155
  Copyright terms: Public domain W3C validator