Theorem necon3bi 2960

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 157	. 2 ⊢ (¬ 𝜑 → ¬ 𝐴 = 𝐵)
3	2	neqned 2941	1 ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2934

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 210  df-ne 2935

This theorem is referenced by:  r19.2zb  4382  pwne  5217  onnevOLD  6294  alephord  9575  ackbij1lem18  9737  fin23lem26  9825  fin1a2lem6  9905  alephom  10085  gchxpidm  10169  egt2lt3  15651  nn0onn  15825  prmodvdslcmf  16483  symgfix2  18662  alexsubALTlem2  22799  alexsubALTlem4  22801  ptcmplem2  22804  nmoid  23495  cxplogb  25524  axlowdimlem17  26904  frgrncvvdeq  28246  hashxpe  30702  hasheuni  31623  limsucncmpi  34272  matunitlindflem1  35396  poimirlem32  35432  ovoliunnfl  35442  voliunnfl  35444  volsupnfl  35445  dvasin  35484  lsat0cv  36670  metakunt24  39739  pellexlem5  40227  uzfissfz  42403  xralrple2  42431  infxr  42444  icccncfext  42970  ioodvbdlimc1lem1  43014  volioc  43055  fourierdlem32  43222  fourierdlem49  43238  fourierdlem73  43262  fourierswlem  43313  fouriersw  43314  sge0pr  43474  voliunsge0lem  43552  carageniuncl  43603  isomenndlem  43610  hoimbl  43711