Theorem necon3bi 3013

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  r19.2zb  4399  pwne  5216  onnevOLD  6280  alephord  9486  ackbij1lem18  9648  fin23lem26  9736  fin1a2lem6  9816  alephom  9996  gchxpidm  10080  egt2lt3  15551  nn0onn  15721  prmodvdslcmf  16373  symgfix2  18536  alexsubALTlem2  22653  alexsubALTlem4  22655  ptcmplem2  22658  nmoid  23348  cxplogb  25372  axlowdimlem17  26752  frgrncvvdeq  28094  hashxpe  30555  hasheuni  31454  limsucncmpi  33906  matunitlindflem1  35053  poimirlem32  35089  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  dvasin  35141  lsat0cv  36329  metakunt24  39373  pellexlem5  39774  uzfissfz  41958  xralrple2  41986  infxr  41999  icccncfext  42529  ioodvbdlimc1lem1  42573  volioc  42614  fourierdlem32  42781  fourierdlem49  42797  fourierdlem73  42821  fourierswlem  42872  fouriersw  42873  sge0pr  43033  voliunsge0lem  43111  carageniuncl  43162  isomenndlem  43169  hoimbl  43270