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

Theorem necon3bi 2689
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 2663 1  |-  ( -. 
ph  ->  A  =/=  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1374    =/= wne 2655
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 2657
This theorem is referenced by:  r19.2zb  3911  pwne  4606  pwne0  4610  onnev  5075  alephord  8445  ackbij1lem18  8606  fin23lem26  8694  fin1a2lem6  8774  alephom  8949  gchxpidm  9036  egt2lt3  13789  symgfix2  16229  chfacfisf  19115  chfacfisfcpmat  19116  alexsubALTlem2  20276  alexsubALTlem4  20278  ptcmplem2  20281  nmoid  20977  axlowdimlem17  23930  2trllemA  24214  2pthon  24266  2pthon3v  24268  frgrancvvdeqlem3  24695  frgrancvvdeqlem9  24704  logccne0OLD  27637  hasheuni  27717  limsucncmpi  29473  ovoliunnfl  29620  voliunnfl  29622  volsupnfl  29623  dvasin  29667  pellexlem5  30360  ioodvbdlimc1lem1  31216  volioc  31245  dirkercncf  31362  fourierdlem32  31394  fourierdlem45  31407  fourierdlem49  31411  fourierdlem73  31435  fourierdlem79  31441  fourierdlem89  31451  fourierdlem91  31453  fouriersw  31487  lsat0cv  33705
  Copyright terms: Public domain W3C validator