Theorem necon3i 2989

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

Syntax hints:   → wi 4   = wceq 1560   ≠ wne 2957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-ne 2958

This theorem is referenced by:  difn0  4320  imadisjlnd  6070  xpnz  6144  unixp  6269  inf3lem2  9584  infeq5  9592  cantnflem1  9644  iunfictbso  10070  rankcf  10735  hashfun  14450  hashge3el3dif  14500  abssubne0  15344  expnprm  16938  grpn0  19013  pmtr3ncomlem2  19514  pgpfaclem2  20124  isdrng2  20789  gzrngunit  21482  zringunit  21515  prmirredlem  21521  uvcf1  21841  lindfrn  21870  mpfrcl  22135  ply1frcl  22378  dfac14lem  23674  flimclslem  24041  lebnumlem3  25022  pmltpclem2  25508  i1fmullem  25753  fta1glem1  26225  fta1blem  26228  dgrcolem1  26330  plydivlem4  26357  plyrem  26366  facth  26367  fta1lem  26368  vieta1lem1  26371  vieta1lem2  26372  vieta1  26373  aalioulem2  26394  geolim3  26400  logcj  26668  argregt0  26672  argimgt0  26674  argimlt0  26675  logneg2  26677  tanarg  26681  logtayl  26722  cxpsqrt  26765  cxpcn3lem  26809  cxpcn3  26810  dcubic2  26906  dcubic  26908  cubic  26911  asinlem  26930  atandmcj  26971  atancj  26972  atanlogsublem  26977  bndatandm  26991  birthdaylem1  27013  basellem4  27145  dchrn0  27311  lgsne0  27396  usgr2trlncl  29957  nmlno0lem  30993  nmlnop0iALT  32195  eldmne0  32826  preimane  32868  ricnzr1  33469  prmidl0  33634  psrnzr  33806  constrrtll  34025  cntnevol  34522  signsvtn0  34861  signstfveq0a  34867  signstfveq0  34868  nepss  36065  elima4  36123  dfttc4lem2  36886  heicant  38151  totbndbnd  38285  cdleme3c  40851  cdleme7e  40868  sn-1ne2  42877  sn-0ne2  43012  uvcn0  43157  compne  45013  stoweidlem39  46610  sinnpoly  47482  rrx2vlinest  49360  rrx2linesl  49362  elfvne0  49467  lanrcl  50239  ranrcl  50240  rellan  50241  relran  50242