Theorem necon3i 2960

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

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

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 2929

This theorem is referenced by:  difn0  4312  imadisjlnd  6025  xpnz  6101  unixp  6224  inf3lem2  9514  infeq5  9522  cantnflem1  9574  iunfictbso  10000  rankcf  10663  hashfun  14339  hashge3el3dif  14389  abssubne0  15219  expnprm  16809  grpn0  18879  pmtr3ncomlem2  19381  pgpfaclem2  19991  isdrng2  20653  gzrngunit  21365  zringunit  21398  prmirredlem  21404  uvcf1  21724  lindfrn  21753  mpfrcl  22015  ply1frcl  22228  dfac14lem  23527  flimclslem  23894  lebnumlem3  24884  pmltpclem2  25372  i1fmullem  25617  fta1glem1  26095  fta1blem  26098  dgrcolem1  26201  plydivlem4  26226  plyrem  26235  facth  26236  fta1lem  26237  vieta1lem1  26240  vieta1lem2  26241  vieta1  26242  aalioulem2  26263  geolim3  26269  logcj  26537  argregt0  26541  argimgt0  26543  argimlt0  26544  logneg2  26546  tanarg  26550  logtayl  26591  cxpsqrt  26634  cxpcn3lem  26679  cxpcn3  26680  dcubic2  26776  dcubic  26778  cubic  26781  asinlem  26800  atandmcj  26841  atancj  26842  atanlogsublem  26847  bndatandm  26861  birthdaylem1  26883  basellem4  27016  dchrn0  27183  lgsne0  27268  usgr2trlncl  29733  nmlno0lem  30765  nmlnop0iALT  31967  eldmne0  32601  preimane  32644  prmidl0  33407  constrrtll  33736  cntnevol  34233  signsvtn0  34575  signstfveq0a  34581  signstfveq0  34582  nepss  35754  elima4  35812  heicant  37695  totbndbnd  37829  cdleme3c  40269  cdleme7e  40286  sn-1ne2  42298  sn-0ne2  42439  uvcn0  42575  compne  44473  stoweidlem39  46077  sinnpoly  46922  rrx2vlinest  48773  rrx2linesl  48775  elfvne0  48880  lanrcl  49653  ranrcl  49654  rellan  49655  relran  49656