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  4455  pwne  5300  alephord  9997  ackbij1lem18  10158  fin23lem26  10247  fin1a2lem6  10327  alephom  10508  gchxpidm  10592  egt2lt3  16143  nn0onn  16319  prmodvdslcmf  16987  chnccat  18561  symgfix2  19357  alexsubALTlem2  24004  alexsubALTlem4  24006  ptcmplem2  24009  nmoid  24698  cxplogb  26764  axlowdimlem17  29043  frgrncvvdeq  30396  hashxpe  32897  hasheuni  34262  fineqvnttrclse  35299  limsucncmpi  36658  matunitlindflem1  37861  poimirlem32  37897  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  dvasin  37949  lsat0cv  39403  unitscyglem4  42562  readvrec2  42725  readvrec  42726  pellexlem5  43184  uzfissfz  45679  xralrple2  45707  infxr  45719  icccncfext  46239  ioodvbdlimc1lem1  46283  volioc  46324  fourierdlem32  46491  fourierdlem49  46507  fourierdlem73  46531  fourierswlem  46582  fouriersw  46583  sge0pr  46746  voliunsge0lem  46824  carageniuncl  46875  isomenndlem  46882  hoimbl  46983