Theorem necon3i 2965

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  difn0  4320  imadisjlnd  6041  xpnz  6118  unixp  6241  inf3lem2  9542  infeq5  9550  cantnflem1  9602  iunfictbso  10028  rankcf  10692  hashfun  14364  hashge3el3dif  14414  abssubne0  15244  expnprm  16834  grpn0  18905  pmtr3ncomlem2  19407  pgpfaclem2  20017  isdrng2  20680  gzrngunit  21392  zringunit  21425  prmirredlem  21431  uvcf1  21751  lindfrn  21780  mpfrcl  22044  ply1frcl  22266  dfac14lem  23565  flimclslem  23932  lebnumlem3  24922  pmltpclem2  25410  i1fmullem  25655  fta1glem1  26133  fta1blem  26136  dgrcolem1  26239  plydivlem4  26264  plyrem  26273  facth  26274  fta1lem  26275  vieta1lem1  26278  vieta1lem2  26279  vieta1  26280  aalioulem2  26301  geolim3  26307  logcj  26575  argregt0  26579  argimgt0  26581  argimlt0  26582  logneg2  26584  tanarg  26588  logtayl  26629  cxpsqrt  26672  cxpcn3lem  26717  cxpcn3  26718  dcubic2  26814  dcubic  26816  cubic  26819  asinlem  26838  atandmcj  26879  atancj  26880  atanlogsublem  26885  bndatandm  26899  birthdaylem1  26921  basellem4  27054  dchrn0  27221  lgsne0  27306  usgr2trlncl  29816  nmlno0lem  30851  nmlnop0iALT  32053  eldmne0  32687  preimane  32729  prmidl0  33512  constrrtll  33869  cntnevol  34366  signsvtn0  34708  signstfveq0a  34714  signstfveq0  34715  nepss  35893  elima4  35951  heicant  37827  totbndbnd  37961  cdleme3c  40527  cdleme7e  40544  sn-1ne2  42556  sn-0ne2  42697  uvcn0  42833  compne  44717  stoweidlem39  46319  sinnpoly  47173  rrx2vlinest  49023  rrx2linesl  49025  elfvne0  49130  lanrcl  49902  ranrcl  49903  rellan  49904  relran  49905