Theorem necon3bi 2958

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	⊢ (𝐴 = 𝐵 → 𝜑)

Assertion

Ref	Expression
necon3bi	⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem necon3bi

Step	Hyp	Ref	Expression
1		necon3bi.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝜑)
2	1	con3i 154	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2939	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  r19.2zb  4440  pwne  5294  alephord  9997  ackbij1lem18  10158  fin23lem26  10247  fin1a2lem6  10327  alephom  10508  gchxpidm  10592  egt2lt3  16173  nn0onn  16349  prmodvdslcmf  17018  chnccat  18592  symgfix2  19391  alexsubALTlem2  24013  alexsubALTlem4  24015  ptcmplem2  24018  nmoid  24707  cxplogb  26750  axlowdimlem17  29027  frgrncvvdeq  30379  hashxpe  32880  hasheuni  34229  fineqvnttrclse  35268  limsucncmpi  36627  matunitlindflem1  37937  poimirlem32  37973  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  dvasin  38025  lsat0cv  39479  unitscyglem4  42637  readvrec2  42793  readvrec  42794  pellexlem5  43261  uzfissfz  45756  xralrple2  45784  infxr  45796  icccncfext  46315  ioodvbdlimc1lem1  46359  volioc  46400  fourierdlem32  46567  fourierdlem49  46583  fourierdlem73  46607  fourierswlem  46658  fouriersw  46659  sge0pr  46822  voliunsge0lem  46900  carageniuncl  46951  isomenndlem  46958  hoimbl  47059