Theorem necon3i 2977

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

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

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 2945

This theorem is referenced by:  difn0  4303  xpnz  6059  unixp  6182  inf3lem2  9348  infeq5  9356  cantnflem1  9408  iunfictbso  9854  rankcf  10517  hashfun  14133  hashge3el3dif  14181  abssubne0  15009  expnprm  16584  grpn0  18592  pmtr3ncomlem2  19063  pgpfaclem2  19666  isdrng2  19982  gzrngunit  20645  zringunit  20669  prmirredlem  20675  uvcf1  20980  lindfrn  21009  mpfrcl  21276  ply1frcl  21465  dfac14lem  22749  flimclslem  23116  lebnumlem3  24107  pmltpclem2  24594  i1fmullem  24839  fta1glem1  25311  fta1blem  25314  dgrcolem1  25415  plydivlem4  25437  plyrem  25446  facth  25447  fta1lem  25448  vieta1lem1  25451  vieta1lem2  25452  vieta1  25453  aalioulem2  25474  geolim3  25480  logcj  25742  argregt0  25746  argimgt0  25748  argimlt0  25749  logneg2  25751  tanarg  25755  logtayl  25796  cxpsqrt  25839  cxpcn3lem  25881  cxpcn3  25882  dcubic2  25975  dcubic  25977  cubic  25980  asinlem  25999  atandmcj  26040  atancj  26041  atanlogsublem  26046  bndatandm  26060  birthdaylem1  26082  basellem4  26214  dchrn0  26379  lgsne0  26464  usgr2trlncl  28107  nmlno0lem  29134  nmlnop0iALT  30336  eldmne0  30942  preimane  30986  prmidl0  31605  cntnevol  32175  signsvtn0  32528  signstfveq0a  32534  signstfveq0  32535  nepss  33641  elima4  33729  heicant  35791  totbndbnd  35926  cdleme3c  38223  cdleme7e  38240  uvcn0  40245  sn-1ne2  40275  sn-0ne2  40369  imadisjlnd  41724  compne  42012  stoweidlem39  43534  rrx2vlinest  46039  rrx2linesl  46041  elfvne0  46128