Theorem necon3bi 2985

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

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

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 2960

This theorem is used by:  r19.2zb  4459  pwne  5318  alephord  10181  ackbij1lem18  10341  fin23lem26  10430  fin1a2lem6  10510  alephom  10697  gchxpidm  10781  egt2lt3  16403  nn0onn  16579  prmodvdslcmf  17254  chnccat  18829  symgfix2  19660  matunitlindflem1  23024  alexsubALTlem2  24397  alexsubALTlem4  24399  ptcmplem2  24402  nmoid  25091  cxplogb  27144  axlowdimlem17  29566  frgrncvvdeq  30940  hashxpe  33469  hasheuni  34787  fineqvnttrclse  35892  limsucncmpi  37411  poimirlem32  38762  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  dvasin  38814  lsat0cv  40282  unitscyglem4  43440  readvrec2  43605  readvrec  43606  pellexlem5  44033  uzfissfz  46543  xralrple2  46571  infxr  46583  icccncfext  47102  ioodvbdlimc1lem1  47146  volioc  47187  fourierdlem32  47354  fourierdlem49  47370  fourierdlem73  47394  fourierswlem  47445  fouriersw  47446  sge0pr  47609  voliunsge0lem  47687  carageniuncl  47738  isomenndlem  47745  hoimbl  47846