Theorem necon3i 2987

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ≠ wne 2955

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 2956

This theorem is used by:  difn0  4314  imadisjlnd  6080  xpnz  6152  unixp  6288  inf3lem2  9637  infeq5  9645  cantnflem1  9697  iunfictbso  10200  rankcf  10869  hashfun  14589  hashge3el3dif  14639  abssubne0  15493  expnprm  17089  grpn0  19191  pmtr3ncomlem2  19697  pgpfaclem2  20307  isdrng2  21006  prmidl0  21643  gzrngunit  21748  zringunit  21781  prmirredlem  21787  uvcf1  22107  lindfrn  22136  mpfrcl  22403  ply1frcl  22645  dfac14lem  23945  flimclslem  24312  lebnumlem3  25293  pmltpclem2  25779  i1fmullem  26024  fta1glem1  26495  fta1blem  26498  dgrcolem1  26601  plydivlem4  26626  plyrem  26635  facth  26636  fta1lem  26637  vieta1lem1  26642  vieta1lem2  26643  vieta1  26644  aalioulem2  26669  geolim3  26675  logcj  26943  argregt0  26947  argimgt0  26949  argimlt0  26950  logneg2  26952  tanarg  26956  logtayl  26997  cxpsqrt  27040  cxpcn3lem  27084  cxpcn3  27085  dcubic2  27181  dcubic  27183  cubic  27186  asinlem  27205  atandmcj  27246  atancj  27247  atanlogsublem  27252  bndatandm  27266  birthdaylem1  27288  basellem4  27420  dchrn0  27586  lgsne0  27671  usgr2trlncl  30355  nmlno0lem  31404  nmlnop0iALT  32606  eldmne0  33272  preimane  33314  ricnzr1  33899  psrnzr  34194  constrrtll  34413  cntnevol  34911  signsvtn0  35249  signstfveq0a  35255  signstfveq0  35256  nepss  36579  elima4  36636  dfttc4lem2  37413  heicant  38682  totbndbnd  38832  cdleme3c  41396  cdleme7e  41413  sn-1ne2  43439  sn-0ne2  43566  uvcn0  43715  compne  45532  stoweidlem39  47157  sinnpoly  48049  rrx2vlinest  49961  rrx2linesl  49963  elfvne0  50068  fuconuniqlem  50889  lanrcl  50912  ranrcl  50913  rellan  50914  relran  50915