Theorem necon3bi 2986

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  r19.2zb  4457  pwne  5314  alephord  10047  ackbij1lem18  10207  fin23lem26  10297  fin1a2lem6  10377  alephom  10558  gchxpidm  10642  egt2lt3  16252  nn0onn  16428  prmodvdslcmf  17097  chnccat  18672  symgfix2  19477  alexsubALTlem2  24166  alexsubALTlem4  24168  ptcmplem2  24171  nmoid  24860  cxplogb  26909  axlowdimlem17  29217  frgrncvvdeq  30569  hashxpe  33064  hasheuni  34392  fineqvnttrclse  35432  limsucncmpi  36818  matunitlindflem1  38127  poimirlem32  38163  ovoliunnfl  38173  voliunnfl  38175  volsupnfl  38176  dvasin  38215  lsat0cv  39669  unitscyglem4  42827  readvrec2  42982  readvrec  42983  pellexlem5  43422  uzfissfz  45900  xralrple2  45928  infxr  45940  icccncfext  46459  ioodvbdlimc1lem1  46503  volioc  46544  fourierdlem32  46711  fourierdlem49  46727  fourierdlem73  46751  fourierswlem  46802  fouriersw  46803  sge0pr  46966  voliunsge0lem  47044  carageniuncl  47095  isomenndlem  47102  hoimbl  47203