Theorem necon3bi 2983

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2958

This theorem is used by:  r19.2zb  4459  pwne  5321  alephord  10082  ackbij1lem18  10242  fin23lem26  10331  fin1a2lem6  10411  alephom  10598  gchxpidm  10682  egt2lt3  16300  nn0onn  16476  prmodvdslcmf  17145  chnccat  18720  symgfix2  19549  matunitlindflem1  22907  alexsubALTlem2  24280  alexsubALTlem4  24282  ptcmplem2  24285  nmoid  24974  cxplogb  27031  axlowdimlem17  29423  frgrncvvdeq  30797  hashxpe  33286  hasheuni  34603  fineqvnttrclse  35658  limsucncmpi  37072  poimirlem32  38409  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  dvasin  38461  lsat0cv  39914  unitscyglem4  43072  readvrec2  43244  readvrec  43245  pellexlem5  43682  uzfissfz  46164  xralrple2  46192  infxr  46204  icccncfext  46723  ioodvbdlimc1lem1  46767  volioc  46808  fourierdlem32  46975  fourierdlem49  46991  fourierdlem73  47015  fourierswlem  47066  fouriersw  47067  sge0pr  47230  voliunsge0lem  47308  carageniuncl  47359  isomenndlem  47366  hoimbl  47467