Theorem necon3bi 2981

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

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

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 2956

This theorem is used by:  r19.2zb  4455  pwne  5313  alephord  10157  ackbij1lem18  10317  fin23lem26  10406  fin1a2lem6  10486  alephom  10673  gchxpidm  10757  egt2lt3  16379  nn0onn  16555  prmodvdslcmf  17230  chnccat  18805  symgfix2  19635  matunitlindflem1  22999  alexsubALTlem2  24372  alexsubALTlem4  24374  ptcmplem2  24377  nmoid  25066  cxplogb  27119  axlowdimlem17  29541  frgrncvvdeq  30915  hashxpe  33445  hasheuni  34763  fineqvnttrclse  35848  limsucncmpi  37325  poimirlem32  38663  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  dvasin  38715  lsat0cv  40183  unitscyglem4  43341  readvrec2  43505  readvrec  43506  pellexlem5  43933  uzfissfz  46431  xralrple2  46459  infxr  46471  icccncfext  46990  ioodvbdlimc1lem1  47034  volioc  47075  fourierdlem32  47242  fourierdlem49  47258  fourierdlem73  47282  fourierswlem  47333  fouriersw  47334  sge0pr  47497  voliunsge0lem  47575  carageniuncl  47626  isomenndlem  47633  hoimbl  47734