Theorem necon3i 2996

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

Syntax hints:   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  difn0  4330  imadisjlnd  6084  xpnz  6157  unixp  6284  inf3lem2  9597  infeq5  9605  cantnflem1  9657  iunfictbso  10097  rankcf  10761  hashfun  14473  hashge3el3dif  14523  abssubne0  15367  expnprm  16961  grpn0  19037  pmtr3ncomlem2  19543  pgpfaclem2  20153  isdrng2  20826  prmidl0  21446  gzrngunit  21551  zringunit  21584  prmirredlem  21590  uvcf1  21910  lindfrn  21939  mpfrcl  22204  ply1frcl  22446  dfac14lem  23742  flimclslem  24109  lebnumlem3  25090  pmltpclem2  25576  i1fmullem  25821  fta1glem1  26293  fta1blem  26296  dgrcolem1  26398  plydivlem4  26425  plyrem  26434  facth  26435  fta1lem  26436  vieta1lem1  26439  vieta1lem2  26440  vieta1  26441  aalioulem2  26462  geolim3  26468  logcj  26736  argregt0  26740  argimgt0  26742  argimlt0  26743  logneg2  26745  tanarg  26749  logtayl  26790  cxpsqrt  26833  cxpcn3lem  26877  cxpcn3  26878  dcubic2  26974  dcubic  26976  cubic  26979  asinlem  26998  atandmcj  27039  atancj  27040  atanlogsublem  27045  bndatandm  27059  birthdaylem1  27081  basellem4  27213  dchrn0  27379  lgsne0  27464  usgr2trlncl  30049  nmlno0lem  31085  nmlnop0iALT  32287  eldmne0  32912  preimane  32954  ricnzr1  33548  psrnzr  33846  constrrtll  34065  cntnevol  34562  signsvtn0  34901  signstfveq0a  34907  signstfveq0  34908  nepss  36108  elima4  36166  dfttc4lem2  36928  heicant  38193  totbndbnd  38327  cdleme3c  40893  cdleme7e  40910  sn-1ne2  42921  sn-0ne2  43056  uvcn0  43201  compne  45041  stoweidlem39  46644  sinnpoly  47516  rrx2vlinest  49405  rrx2linesl  49407  elfvne0  49511  lanrcl  50283  ranrcl  50284  rellan  50285  relran  50286