Theorem necon3bi 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  r19.2zb  4423  pwne  5268  onnevOLD  6373  alephord  9762  ackbij1lem18  9924  fin23lem26  10012  fin1a2lem6  10092  alephom  10272  gchxpidm  10356  egt2lt3  15843  nn0onn  16017  prmodvdslcmf  16676  symgfix2  18939  alexsubALTlem2  23107  alexsubALTlem4  23109  ptcmplem2  23112  nmoid  23812  cxplogb  25841  axlowdimlem17  27229  frgrncvvdeq  28574  hashxpe  31029  hasheuni  31953  limsucncmpi  34561  matunitlindflem1  35700  poimirlem32  35736  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  dvasin  35788  lsat0cv  36974  metakunt24  40076  pellexlem5  40571  uzfissfz  42755  xralrple2  42783  infxr  42796  icccncfext  43318  ioodvbdlimc1lem1  43362  volioc  43403  fourierdlem32  43570  fourierdlem49  43586  fourierdlem73  43610  fourierswlem  43661  fouriersw  43662  sge0pr  43822  voliunsge0lem  43900  carageniuncl  43951  isomenndlem  43958  hoimbl  44059