Theorem necon3i 2990

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

Syntax hints:   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  difn0  4322  imadisjlnd  6083  xpnz  6156  unixp  6283  inf3lem2  9594  infeq5  9602  cantnflem1  9654  iunfictbso  10094  rankcf  10757  hashfun  14470  hashge3el3dif  14520  abssubne0  15364  expnprm  16957  grpn0  19033  pmtr3ncomlem2  19539  pgpfaclem2  20149  isdrng2  20843  prmidl0  21478  gzrngunit  21583  zringunit  21616  prmirredlem  21622  uvcf1  21942  lindfrn  21971  mpfrcl  22236  ply1frcl  22478  dfac14lem  23774  flimclslem  24141  lebnumlem3  25122  pmltpclem2  25608  i1fmullem  25853  fta1glem1  26325  fta1blem  26328  dgrcolem1  26430  plydivlem4  26457  plyrem  26466  facth  26467  fta1lem  26468  vieta1lem1  26471  vieta1lem2  26472  vieta1  26473  aalioulem2  26496  geolim3  26502  logcj  26771  argregt0  26775  argimgt0  26777  argimlt0  26778  logneg2  26780  tanarg  26784  logtayl  26825  cxpsqrt  26868  cxpcn3lem  26912  cxpcn3  26913  dcubic2  27009  dcubic  27011  cubic  27014  asinlem  27033  atandmcj  27074  atancj  27075  atanlogsublem  27080  bndatandm  27094  birthdaylem1  27116  basellem4  27248  dchrn0  27414  lgsne0  27499  usgr2trlncl  30109  nmlno0lem  31145  nmlnop0iALT  32347  eldmne0  32972  preimane  33014  ricnzr1  33608  psrnzr  33902  constrrtll  34121  cntnevol  34618  signsvtn0  34957  signstfveq0a  34963  signstfveq0  34964  nepss  36210  elima4  36268  dfttc4lem2  37040  heicant  38306  totbndbnd  38440  cdleme3c  41004  cdleme7e  41021  sn-1ne2  43032  sn-0ne2  43167  uvcn0  43310  compne  45150  stoweidlem39  46753  sinnpoly  47628  rrx2vlinest  49521  rrx2linesl  49523  elfvne0  49627  lanrcl  50399  ranrcl  50400  rellan  50401  relran  50402