Theorem necon3i 2992

Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon3i.1	⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)

Assertion

Ref	Expression
necon3i	⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)

Proof of Theorem necon3i

Step	Hyp	Ref	Expression
1		necon3i.1	. . 3 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷)
2	1	necon3ai 2985	. 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵)
3	2	neqned 2967	1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2960

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 2961

This theorem is used by:  difn0  4322  imadisjlnd  6085  xpnz  6158  unixp  6287  inf3lem2  9605  infeq5  9613  cantnflem1  9665  iunfictbso  10114  rankcf  10777  hashfun  14492  hashge3el3dif  14542  abssubne0  15392  expnprm  16984  grpn0  19082  pmtr3ncomlem2  19588  pgpfaclem2  20198  isdrng2  20893  prmidl0  21528  gzrngunit  21633  zringunit  21666  prmirredlem  21672  uvcf1  21992  lindfrn  22021  mpfrcl  22286  ply1frcl  22528  dfac14lem  23825  flimclslem  24192  lebnumlem3  25173  pmltpclem2  25659  i1fmullem  25904  fta1glem1  26376  fta1blem  26379  dgrcolem1  26481  plydivlem4  26508  plyrem  26517  facth  26518  fta1lem  26519  vieta1lem1  26522  vieta1lem2  26523  vieta1  26524  aalioulem2  26547  geolim3  26553  logcj  26822  argregt0  26826  argimgt0  26828  argimlt0  26829  logneg2  26831  tanarg  26835  logtayl  26876  cxpsqrt  26919  cxpcn3lem  26963  cxpcn3  26964  dcubic2  27060  dcubic  27062  cubic  27065  asinlem  27084  atandmcj  27125  atancj  27126  atanlogsublem  27131  bndatandm  27145  birthdaylem1  27167  basellem4  27299  dchrn0  27465  lgsne0  27550  usgr2trlncl  30173  nmlno0lem  31216  nmlnop0iALT  32418  eldmne0  33043  preimane  33085  ricnzr1  33672  psrnzr  33966  constrrtll  34185  cntnevol  34683  signsvtn0  35022  signstfveq0a  35028  signstfveq0  35029  nepss  36247  elima4  36305  dfttc4lem2  37097  heicant  38363  totbndbnd  38498  cdleme3c  41062  cdleme7e  41079  sn-1ne2  43090  sn-0ne2  43225  uvcn0  43368  compne  45208  stoweidlem39  46811  sinnpoly  47686  rrx2vlinest  49578  rrx2linesl  49580  elfvne0  49684  lanrcl  50456  ranrcl  50457  rellan  50458  relran  50459