Theorem necon3bi 2967

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  r19.2zb  4495  pwne  5350  onnevOLD  6492  alephord  10072  ackbij1lem18  10234  fin23lem26  10322  fin1a2lem6  10402  alephom  10582  gchxpidm  10666  egt2lt3  16151  nn0onn  16325  prmodvdslcmf  16982  symgfix2  19286  alexsubALTlem2  23559  alexsubALTlem4  23561  ptcmplem2  23564  nmoid  24266  cxplogb  26298  axlowdimlem17  28254  frgrncvvdeq  29600  hashxpe  32057  hasheuni  33152  limsucncmpi  35416  matunitlindflem1  36570  poimirlem32  36606  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  dvasin  36658  lsat0cv  37989  metakunt24  41094  pellexlem5  41653  uzfissfz  44115  xralrple2  44143  infxr  44156  icccncfext  44682  ioodvbdlimc1lem1  44726  volioc  44767  fourierdlem32  44934  fourierdlem49  44950  fourierdlem73  44974  fourierswlem  45025  fouriersw  45026  sge0pr  45189  voliunsge0lem  45267  carageniuncl  45318  isomenndlem  45325  hoimbl  45426