Theorem necon3bi 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  r19.2zb  4441  pwne  5290  alephord  9988  ackbij1lem18  10149  fin23lem26  10238  fin1a2lem6  10318  alephom  10499  gchxpidm  10583  egt2lt3  16164  nn0onn  16340  prmodvdslcmf  17009  chnccat  18583  symgfix2  19382  alexsubALTlem2  24023  alexsubALTlem4  24025  ptcmplem2  24028  nmoid  24717  cxplogb  26763  axlowdimlem17  29041  frgrncvvdeq  30394  hashxpe  32895  hasheuni  34245  fineqvnttrclse  35284  limsucncmpi  36643  matunitlindflem1  37951  poimirlem32  37987  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  dvasin  38039  lsat0cv  39493  unitscyglem4  42651  readvrec2  42807  readvrec  42808  pellexlem5  43279  uzfissfz  45774  xralrple2  45802  infxr  45814  icccncfext  46333  ioodvbdlimc1lem1  46377  volioc  46418  fourierdlem32  46585  fourierdlem49  46601  fourierdlem73  46625  fourierswlem  46676  fouriersw  46677  sge0pr  46840  voliunsge0lem  46918  carageniuncl  46969  isomenndlem  46976  hoimbl  47077