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  10069  ackbij1lem18  10231  fin23lem26  10319  fin1a2lem6  10399  alephom  10579  gchxpidm  10663  egt2lt3  16148  nn0onn  16322  prmodvdslcmf  16979  symgfix2  19283  alexsubALTlem2  23551  alexsubALTlem4  23553  ptcmplem2  23556  nmoid  24258  cxplogb  26288  axlowdimlem17  28213  frgrncvvdeq  29559  hashxpe  32014  hasheuni  33078  limsucncmpi  35325  matunitlindflem1  36479  poimirlem32  36515  ovoliunnfl  36525  voliunnfl  36527  volsupnfl  36528  dvasin  36567  lsat0cv  37898  metakunt24  41003  pellexlem5  41561  uzfissfz  44026  xralrple2  44054  infxr  44067  icccncfext  44593  ioodvbdlimc1lem1  44637  volioc  44678  fourierdlem32  44845  fourierdlem49  44861  fourierdlem73  44885  fourierswlem  44936  fouriersw  44937  sge0pr  45100  voliunsge0lem  45178  carageniuncl  45229  isomenndlem  45236  hoimbl  45337