Theorem necon3bi 3042

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  r19.2zb  4440  pwne  5250  onnev  6310  alephord  9500  ackbij1lem18  9658  fin23lem26  9746  fin1a2lem6  9826  alephom  10006  gchxpidm  10090  egt2lt3  15558  nn0onn  15730  prmodvdslcmf  16382  symgfix2  18543  alexsubALTlem2  22655  alexsubALTlem4  22657  ptcmplem2  22660  nmoid  23350  cxplogb  25363  axlowdimlem17  26743  frgrncvvdeq  28087  hashxpe  30528  hasheuni  31344  limsucncmpi  33793  matunitlindflem1  34887  poimirlem32  34923  ovoliunnfl  34933  voliunnfl  34935  volsupnfl  34936  dvasin  34977  lsat0cv  36168  pellexlem5  39428  uzfissfz  41592  xralrple2  41620  infxr  41633  icccncfext  42168  ioodvbdlimc1lem1  42214  volioc  42255  fourierdlem32  42423  fourierdlem49  42439  fourierdlem73  42463  fourierswlem  42514  fouriersw  42515  sge0pr  42675  voliunsge0lem  42753  carageniuncl  42804  isomenndlem  42811  hoimbl  42912