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

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

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