Theorem necon3bi 2982

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 2963	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  r19.2zb  4453  pwne  5308  alephord  10028  ackbij1lem18  10189  fin23lem26  10279  fin1a2lem6  10359  alephom  10540  gchxpidm  10624  egt2lt3  16221  nn0onn  16397  prmodvdslcmf  17066  chnccat  18641  symgfix2  19439  alexsubALTlem2  24088  alexsubALTlem4  24090  ptcmplem2  24093  nmoid  24782  cxplogb  26828  axlowdimlem17  29105  frgrncvvdeq  30457  hashxpe  32959  hasheuni  34343  fineqvnttrclse  35384  limsucncmpi  36769  matunitlindflem1  38079  poimirlem32  38115  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  dvasin  38167  lsat0cv  39621  unitscyglem4  42779  readvrec2  42934  readvrec  42935  pellexlem5  43374  uzfissfz  45866  xralrple2  45894  infxr  45906  icccncfext  46425  ioodvbdlimc1lem1  46469  volioc  46510  fourierdlem32  46677  fourierdlem49  46693  fourierdlem73  46717  fourierswlem  46768  fouriersw  46769  sge0pr  46932  voliunsge0lem  47010  carageniuncl  47061  isomenndlem  47068  hoimbl  47169