Theorem necon3i 2970

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  difn0  4372  imadisjlnd  6100  xpnz  6180  unixp  6303  inf3lem2  9666  infeq5  9674  cantnflem1  9726  iunfictbso  10151  rankcf  10814  hashfun  14472  hashge3el3dif  14522  abssubne0  15351  expnprm  16935  grpn0  19001  pmtr3ncomlem2  19506  pgpfaclem2  20116  isdrng2  20759  gzrngunit  21468  zringunit  21494  prmirredlem  21500  uvcf1  21829  lindfrn  21858  mpfrcl  22126  ply1frcl  22337  dfac14lem  23640  flimclslem  24007  lebnumlem3  25008  pmltpclem2  25497  i1fmullem  25742  fta1glem1  26221  fta1blem  26224  dgrcolem1  26327  plydivlem4  26352  plyrem  26361  facth  26362  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  vieta1  26368  aalioulem2  26389  geolim3  26395  logcj  26662  argregt0  26666  argimgt0  26668  argimlt0  26669  logneg2  26671  tanarg  26675  logtayl  26716  cxpsqrt  26759  cxpcn3lem  26804  cxpcn3  26805  dcubic2  26901  dcubic  26903  cubic  26906  asinlem  26925  atandmcj  26966  atancj  26967  atanlogsublem  26972  bndatandm  26986  birthdaylem1  27008  basellem4  27141  dchrn0  27308  lgsne0  27393  usgr2trlncl  29792  nmlno0lem  30821  nmlnop0iALT  32023  eldmne0  32644  preimane  32686  prmidl0  33457  constrrtll  33736  cntnevol  34208  signsvtn0  34563  signstfveq0a  34569  signstfveq0  34570  nepss  35697  elima4  35756  heicant  37641  totbndbnd  37775  cdleme3c  40212  cdleme7e  40229  sn-1ne2  42278  sn-0ne2  42412  uvcn0  42528  compne  44436  stoweidlem39  45994  rrx2vlinest  48590  rrx2linesl  48592  elfvne0  48678