Theorem necon3i 2966

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  difn0  4295  imadisjlnd  6033  xpnz  6110  unixp  6233  inf3lem2  9541  infeq5  9549  cantnflem1  9601  iunfictbso  10027  rankcf  10691  hashfun  14390  hashge3el3dif  14440  abssubne0  15270  expnprm  16864  grpn0  18938  pmtr3ncomlem2  19440  pgpfaclem2  20050  isdrng2  20715  gzrngunit  21408  zringunit  21441  prmirredlem  21447  uvcf1  21767  lindfrn  21796  mpfrcl  22061  ply1frcl  22304  dfac14lem  23600  flimclslem  23967  lebnumlem3  24948  pmltpclem2  25434  i1fmullem  25679  fta1glem1  26151  fta1blem  26154  dgrcolem1  26256  plydivlem4  26280  plyrem  26289  facth  26290  fta1lem  26291  vieta1lem1  26294  vieta1lem2  26295  vieta1  26296  aalioulem2  26317  geolim3  26323  logcj  26588  argregt0  26592  argimgt0  26594  argimlt0  26595  logneg2  26597  tanarg  26601  logtayl  26642  cxpsqrt  26685  cxpcn3lem  26729  cxpcn3  26730  dcubic2  26826  dcubic  26828  cubic  26831  asinlem  26850  atandmcj  26891  atancj  26892  atanlogsublem  26897  bndatandm  26911  birthdaylem1  26933  basellem4  27065  dchrn0  27231  lgsne0  27316  usgr2trlncl  29846  nmlno0lem  30882  nmlnop0iALT  32084  eldmne0  32719  preimane  32761  ricnzr1  33369  prmidl0  33533  psrnzr  33696  constrrtll  33915  cntnevol  34412  signsvtn0  34754  signstfveq0a  34760  signstfveq0  34761  nepss  35946  elima4  36004  dfttc4lem2  36757  heicant  38022  totbndbnd  38156  cdleme3c  40722  cdleme7e  40739  sn-1ne2  42748  sn-0ne2  42883  uvcn0  43028  compne  44884  stoweidlem39  46482  sinnpoly  47354  rrx2vlinest  49232  rrx2linesl  49234  elfvne0  49339  lanrcl  50111  ranrcl  50112  rellan  50113  relran  50114