Theorem necon3bi 2966

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2939

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 2940

This theorem is referenced by:  r19.2zb  4495  pwne  5352  alephord  10116  ackbij1lem18  10277  fin23lem26  10366  fin1a2lem6  10446  alephom  10626  gchxpidm  10710  egt2lt3  16243  nn0onn  16418  prmodvdslcmf  17086  symgfix2  19435  alexsubALTlem2  24057  alexsubALTlem4  24059  ptcmplem2  24062  nmoid  24764  cxplogb  26830  axlowdimlem17  28974  frgrncvvdeq  30329  hashxpe  32812  hasheuni  34087  limsucncmpi  36447  matunitlindflem1  37624  poimirlem32  37660  ovoliunnfl  37670  voliunnfl  37672  volsupnfl  37673  dvasin  37712  lsat0cv  39035  unitscyglem4  42200  metakunt24  42230  readvrec2  42396  readvrec  42397  pellexlem5  42849  uzfissfz  45342  xralrple2  45370  infxr  45383  icccncfext  45907  ioodvbdlimc1lem1  45951  volioc  45992  fourierdlem32  46159  fourierdlem49  46175  fourierdlem73  46199  fourierswlem  46250  fouriersw  46251  sge0pr  46414  voliunsge0lem  46492  carageniuncl  46543  isomenndlem  46550  hoimbl  46651