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

Theorem necon3bi 2681
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 )
32neneqad 2656 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2648
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 2650
This theorem is referenced by:  r19.2zb  3879  pwne  4567  pwne0  4571  onnev  5030  alephord  8357  ackbij1lem18  8518  fin23lem26  8606  fin1a2lem6  8686  alephom  8861  gchxpidm  8948  egt2lt3  13607  symgfix2  16041  alexsubALTlem2  19753  alexsubALTlem4  19755  ptcmplem2  19758  nmoid  20454  axlowdimlem17  23357  2trllemA  23602  2pthon  23654  2pthon3v  23656  logccne0OLD  26600  hasheuni  26680  limsucncmpi  28436  ovoliunnfl  28582  voliunnfl  28584  volsupnfl  28585  dvasin  28629  pellexlem5  29323  frgrancvvdeqlem3  30774  frgrancvvdeqlem9  30783  chfacfisf  31341  chfacfisfcpmat  31342  lsat0cv  33017
  Copyright terms: Public domain W3C validator