Theorem necon3bi 2683

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 2657	1 |- ( -. ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2649

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 2651

This theorem is referenced by:  r19.2zb  3907  pwne  4603  pwne0  4607  onnev  5072  alephord  8447  ackbij1lem18  8608  fin23lem26  8696  fin1a2lem6  8776  alephom  8951  gchxpidm  9036  egt2lt3  14021  symgfix2  16640  chfacfisf  19522  chfacfisfcpmat  19523  alexsubALTlem2  20714  alexsubALTlem4  20716  ptcmplem2  20719  nmoid  21415  cxplogb  23325  axlowdimlem17  24463  2trllemA  24754  2pthon  24806  2pthon3v  24808  frgrancvvdeqlem3  25234  frgrancvvdeqlem9  25243  hasheuni  28314  limsucncmpi  30138  ovoliunnfl  30296  voliunnfl  30298  volsupnfl  30299  dvasin  30343  pellexlem5  31008  icccncfext  31929  ioodvbdlimc1lem1  31967  volioc  32010  fourierdlem32  32160  fourierdlem49  32177  fourierdlem73  32201  fourierswlem  32252  fouriersw  32253  lsat0cv  35155