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

Theorem necon3bi 2672
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 2646 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1383    =/= wne 2638
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 2640
This theorem is referenced by:  r19.2zb  3905  pwne  4603  pwne0  4607  onnev  5074  alephord  8459  ackbij1lem18  8620  fin23lem26  8708  fin1a2lem6  8788  alephom  8963  gchxpidm  9050  egt2lt3  13920  symgfix2  16419  chfacfisf  19332  chfacfisfcpmat  19333  alexsubALTlem2  20525  alexsubALTlem4  20527  ptcmplem2  20530  nmoid  21226  axlowdimlem17  24237  2trllemA  24528  2pthon  24580  2pthon3v  24582  frgrancvvdeqlem3  25008  frgrancvvdeqlem9  25017  logccne0OLD  27988  hasheuni  28068  limsucncmpi  29885  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  dvasin  30078  pellexlem5  30744  icccncfext  31597  ioodvbdlimc1lem1  31632  volioc  31661  fourierdlem32  31810  fourierdlem49  31827  fourierdlem73  31851  fourierswlem  31902  fouriersw  31903  lsat0cv  34498
  Copyright terms: Public domain W3C validator