Theorem necon3bi 2987

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

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

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 2962

This theorem is used by:  r19.2zb  4466  pwne  5328  alephord  10078  ackbij1lem18  10238  fin23lem26  10327  fin1a2lem6  10407  alephom  10588  gchxpidm  10672  egt2lt3  16287  nn0onn  16463  prmodvdslcmf  17132  chnccat  18707  symgfix2  19517  alexsubALTlem2  24242  alexsubALTlem4  24244  ptcmplem2  24247  nmoid  24936  cxplogb  26988  axlowdimlem17  29345  frgrncvvdeq  30697  hashxpe  33189  hasheuni  34506  fineqvnttrclse  35561  limsucncmpi  36997  matunitlindflem1  38308  poimirlem32  38344  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  dvasin  38396  lsat0cv  39848  unitscyglem4  43006  readvrec2  43163  readvrec  43164  pellexlem5  43601  uzfissfz  46083  xralrple2  46111  infxr  46123  icccncfext  46642  ioodvbdlimc1lem1  46686  volioc  46727  fourierdlem32  46894  fourierdlem49  46910  fourierdlem73  46934  fourierswlem  46985  fouriersw  46986  sge0pr  47149  voliunsge0lem  47227  carageniuncl  47278  isomenndlem  47285  hoimbl  47386