Theorem necon3i 2964

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2932

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 2933

This theorem is referenced by:  difn0  4342  imadisjlnd  6068  xpnz  6148  unixp  6271  inf3lem2  9643  infeq5  9651  cantnflem1  9703  iunfictbso  10128  rankcf  10791  hashfun  14455  hashge3el3dif  14505  abssubne0  15335  expnprm  16922  grpn0  18954  pmtr3ncomlem2  19455  pgpfaclem2  20065  isdrng2  20703  gzrngunit  21401  zringunit  21427  prmirredlem  21433  uvcf1  21752  lindfrn  21781  mpfrcl  22043  ply1frcl  22256  dfac14lem  23555  flimclslem  23922  lebnumlem3  24913  pmltpclem2  25402  i1fmullem  25647  fta1glem1  26125  fta1blem  26128  dgrcolem1  26231  plydivlem4  26256  plyrem  26265  facth  26266  fta1lem  26267  vieta1lem1  26270  vieta1lem2  26271  vieta1  26272  aalioulem2  26293  geolim3  26299  logcj  26567  argregt0  26571  argimgt0  26573  argimlt0  26574  logneg2  26576  tanarg  26580  logtayl  26621  cxpsqrt  26664  cxpcn3lem  26709  cxpcn3  26710  dcubic2  26806  dcubic  26808  cubic  26811  asinlem  26830  atandmcj  26871  atancj  26872  atanlogsublem  26877  bndatandm  26891  birthdaylem1  26913  basellem4  27046  dchrn0  27213  lgsne0  27298  usgr2trlncl  29742  nmlno0lem  30774  nmlnop0iALT  31976  eldmne0  32606  preimane  32648  prmidl0  33465  constrrtll  33765  cntnevol  34259  signsvtn0  34602  signstfveq0a  34608  signstfveq0  34609  nepss  35735  elima4  35793  heicant  37679  totbndbnd  37813  cdleme3c  40249  cdleme7e  40266  sn-1ne2  42315  sn-0ne2  42449  uvcn0  42565  compne  44465  stoweidlem39  46068  rrx2vlinest  48721  rrx2linesl  48723  elfvne0  48827  lanrcl  49496  ranrcl  49497  rellan  49498  relran  49499