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

Step	Hyp	Ref	Expression
1		necon3bi.1	. . 3 |- ( A = B -> ph )
2	1	con3i 135	. 2 |- ( -. ph -> -. A = B )
3	2	neqned 2663	1 |- ( -. ph -> A =/= B )

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