Theorem necon3bi 2957

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

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

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 207  df-ne 2932

This theorem is referenced by:  r19.2zb  4476  pwne  5333  alephord  10097  ackbij1lem18  10258  fin23lem26  10347  fin1a2lem6  10427  alephom  10607  gchxpidm  10691  egt2lt3  16225  nn0onn  16400  prmodvdslcmf  17068  symgfix2  19403  alexsubALTlem2  24003  alexsubALTlem4  24005  ptcmplem2  24008  nmoid  24700  cxplogb  26766  axlowdimlem17  28904  frgrncvvdeq  30257  hashxpe  32755  hasheuni  34061  limsucncmpi  36421  matunitlindflem1  37598  poimirlem32  37634  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  dvasin  37686  lsat0cv  39009  unitscyglem4  42174  metakunt24  42204  readvrec2  42370  readvrec  42371  pellexlem5  42822  uzfissfz  45309  xralrple2  45337  infxr  45350  icccncfext  45874  ioodvbdlimc1lem1  45918  volioc  45959  fourierdlem32  46126  fourierdlem49  46142  fourierdlem73  46166  fourierswlem  46217  fouriersw  46218  sge0pr  46381  voliunsge0lem  46459  carageniuncl  46510  isomenndlem  46517  hoimbl  46618