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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  r19.2zb  4456  pwne  5314  alephord  10135  ackbij1lem18  10295  fin23lem26  10384  fin1a2lem6  10464  alephom  10651  gchxpidm  10735  egt2lt3  16354  nn0onn  16530  prmodvdslcmf  17205  chnccat  18780  symgfix2  19610  matunitlindflem1  22974  alexsubALTlem2  24347  alexsubALTlem4  24349  ptcmplem2  24352  nmoid  25041  cxplogb  27096  axlowdimlem17  29518  frgrncvvdeq  30892  hashxpe  33381  hasheuni  34699  fineqvnttrclse  35765  limsucncmpi  37203  poimirlem32  38538  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  dvasin  38590  lsat0cv  40058  unitscyglem4  43216  readvrec2  43380  readvrec  43381  pellexlem5  43793  uzfissfz  46282  xralrple2  46310  infxr  46322  icccncfext  46841  ioodvbdlimc1lem1  46885  volioc  46926  fourierdlem32  47093  fourierdlem49  47109  fourierdlem73  47133  fourierswlem  47184  fouriersw  47185  sge0pr  47348  voliunsge0lem  47426  carageniuncl  47477  isomenndlem  47484  hoimbl  47585