Theorem necon3bi 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2933

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 2934

This theorem is referenced by:  r19.2zb  4476  pwne  5328  alephord  10094  ackbij1lem18  10255  fin23lem26  10344  fin1a2lem6  10424  alephom  10604  gchxpidm  10688  egt2lt3  16229  nn0onn  16404  prmodvdslcmf  17072  symgfix2  19402  alexsubALTlem2  23991  alexsubALTlem4  23993  ptcmplem2  23996  nmoid  24686  cxplogb  26753  axlowdimlem17  28942  frgrncvvdeq  30295  hashxpe  32791  hasheuni  34121  limsucncmpi  36468  matunitlindflem1  37645  poimirlem32  37681  ovoliunnfl  37691  voliunnfl  37693  volsupnfl  37694  dvasin  37733  lsat0cv  39056  unitscyglem4  42216  readvrec2  42371  readvrec  42372  pellexlem5  42823  uzfissfz  45320  xralrple2  45348  infxr  45361  icccncfext  45883  ioodvbdlimc1lem1  45927  volioc  45968  fourierdlem32  46135  fourierdlem49  46151  fourierdlem73  46175  fourierswlem  46226  fouriersw  46227  sge0pr  46390  voliunsge0lem  46468  carageniuncl  46519  isomenndlem  46526  hoimbl  46627