Theorem necon3bi 2669

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 142	. 2 |- ( -. ph -> -. A = B )
3	2	neqned 2650	1 |- ( -. ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1452   =/= wne 2641

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 190  df-ne 2643

This theorem is referenced by:  r19.2zb  3850  pwne  4567  pwne0  4571  onnev  5550  alephord  8524  ackbij1lem18  8685  fin23lem26  8773  fin1a2lem6  8853  alephom  9028  gchxpidm  9112  egt2lt3  14335  prmodvdslcmf  15084  prmordvdslcmfOLD  15098  prmordvdslcmsOLDOLD  15100  symgfix2  17135  chfacfisf  19955  chfacfisfcpmat  19956  alexsubALTlem2  21141  alexsubALTlem4  21143  ptcmplem2  21146  nmoid  21841  cxplogb  23802  axlowdimlem17  25067  2trllemA  25359  2pthon  25411  2pthon3v  25413  frgrancvvdeqlem3  25839  frgrancvvdeqlem9  25848  hasheuni  28980  limsucncmpi  31176  poimirlem32  32036  ovoliunnfl  32046  voliunnfl  32048  volsupnfl  32049  dvasin  32092  lsat0cv  32670  pellexlem5  35748  uzfissfz  37636  xralrple2  37664  infxr  37677  icccncfext  37862  ioodvbdlimc1lem1  37900  ioodvbdlimc1lem1OLD  37902  volioc  37946  fourierdlem32  38114  fourierdlem49  38131  fourierdlem73  38155  fourierswlem  38206  fouriersw  38207  prsal  38291  sge0pr  38350  voliunsge0lem  38426  carageniuncl  38463  isomenndlem  38470  hoimbl  38571