Theorem necon3i 2973

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  difn0  4364  xpnz  6158  unixp  6281  inf3lem2  9626  infeq5  9634  cantnflem1  9686  iunfictbso  10111  rankcf  10774  hashfun  14401  hashge3el3dif  14451  abssubne0  15267  expnprm  16839  grpn0  18892  pmtr3ncomlem2  19383  pgpfaclem2  19993  isdrng2  20514  gzrngunit  21211  zringunit  21237  prmirredlem  21243  uvcf1  21566  lindfrn  21595  mpfrcl  21867  ply1frcl  22057  dfac14lem  23341  flimclslem  23708  lebnumlem3  24703  pmltpclem2  25190  i1fmullem  25435  fta1glem1  25907  fta1blem  25910  dgrcolem1  26011  plydivlem4  26033  plyrem  26042  facth  26043  fta1lem  26044  vieta1lem1  26047  vieta1lem2  26048  vieta1  26049  aalioulem2  26070  geolim3  26076  logcj  26338  argregt0  26342  argimgt0  26344  argimlt0  26345  logneg2  26347  tanarg  26351  logtayl  26392  cxpsqrt  26435  cxpcn3lem  26479  cxpcn3  26480  dcubic2  26573  dcubic  26575  cubic  26578  asinlem  26597  atandmcj  26638  atancj  26639  atanlogsublem  26644  bndatandm  26658  birthdaylem1  26680  basellem4  26812  dchrn0  26977  lgsne0  27062  usgr2trlncl  29272  nmlno0lem  30301  nmlnop0iALT  31503  eldmne0  32107  preimane  32150  prmidl0  32831  cntnevol  33512  signsvtn0  33867  signstfveq0a  33873  signstfveq0  33874  nepss  34979  elima4  35039  heicant  36826  totbndbnd  36960  cdleme3c  39404  cdleme7e  39421  uvcn0  41414  sn-1ne2  41481  sn-0ne2  41581  imadisjlnd  43214  compne  43502  stoweidlem39  45054  rrx2vlinest  47515  rrx2linesl  47517  elfvne0  47603