Theorem necon3bi 3042

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 157	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 3023	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 3017

This theorem is referenced by:  r19.2zb  4441  pwne  5251  onnev  6311  alephord  9501  ackbij1lem18  9659  fin23lem26  9747  fin1a2lem6  9827  alephom  10007  gchxpidm  10091  egt2lt3  15559  nn0onn  15731  prmodvdslcmf  16383  symgfix2  18544  alexsubALTlem2  22656  alexsubALTlem4  22658  ptcmplem2  22661  nmoid  23351  cxplogb  25364  axlowdimlem17  26744  frgrncvvdeq  28088  hashxpe  30529  hasheuni  31344  limsucncmpi  33793  matunitlindflem1  34903  poimirlem32  34939  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  dvasin  34993  lsat0cv  36184  pellexlem5  39450  uzfissfz  41614  xralrple2  41642  infxr  41655  icccncfext  42190  ioodvbdlimc1lem1  42236  volioc  42277  fourierdlem32  42444  fourierdlem49  42460  fourierdlem73  42484  fourierswlem  42535  fouriersw  42536  sge0pr  42696  voliunsge0lem  42774  carageniuncl  42825  isomenndlem  42832  hoimbl  42933