Theorem necon3i 2988

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 2981	. 2 ⊢ (𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵)
3	2	neqned 2963	1 ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)

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

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 2957

This theorem is used by:  difn0  4315  imadisjlnd  6078  xpnz  6150  unixp  6284  inf3lem2  9623  infeq5  9631  cantnflem1  9683  iunfictbso  10186  rankcf  10855  hashfun  14575  hashge3el3dif  14625  abssubne0  15477  expnprm  17073  grpn0  19175  pmtr3ncomlem2  19681  pgpfaclem2  20291  isdrng2  20990  prmidl0  21627  gzrngunit  21732  zringunit  21765  prmirredlem  21771  uvcf1  22091  lindfrn  22120  mpfrcl  22387  ply1frcl  22629  dfac14lem  23929  flimclslem  24296  lebnumlem3  25277  pmltpclem2  25763  i1fmullem  26008  fta1glem1  26479  fta1blem  26482  dgrcolem1  26585  plydivlem4  26610  plyrem  26619  facth  26620  fta1lem  26621  vieta1lem1  26626  vieta1lem2  26627  vieta1  26628  aalioulem2  26653  geolim3  26659  logcj  26927  argregt0  26931  argimgt0  26933  argimlt0  26934  logneg2  26936  tanarg  26940  logtayl  26981  cxpsqrt  27024  cxpcn3lem  27068  cxpcn3  27069  dcubic2  27165  dcubic  27167  cubic  27170  asinlem  27189  atandmcj  27230  atancj  27231  atanlogsublem  27236  bndatandm  27250  birthdaylem1  27272  basellem4  27404  dchrn0  27570  lgsne0  27655  usgr2trlncl  30339  nmlno0lem  31388  nmlnop0iALT  32590  eldmne0  33214  preimane  33256  ricnzr1  33842  psrnzr  34137  constrrtll  34356  cntnevol  34854  signsvtn0  35192  signstfveq0a  35198  signstfveq0  35199  nepss  36462  elima4  36520  dfttc4lem2  37297  heicant  38553  totbndbnd  38703  cdleme3c  41267  cdleme7e  41284  sn-1ne2  43310  sn-0ne2  43437  uvcn0  43586  compne  45409  stoweidlem39  47018  sinnpoly  47910  rrx2vlinest  49822  rrx2linesl  49824  elfvne0  49928  lanrcl  50698  ranrcl  50699  rellan  50700  relran  50701