Theorem necon3i 2965

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  difn0  4308  imadisjlnd  6040  xpnz  6117  unixp  6240  inf3lem2  9541  infeq5  9549  cantnflem1  9601  iunfictbso  10027  rankcf  10691  hashfun  14390  hashge3el3dif  14440  abssubne0  15270  expnprm  16864  grpn0  18938  pmtr3ncomlem2  19440  pgpfaclem2  20050  isdrng2  20711  gzrngunit  21423  zringunit  21456  prmirredlem  21462  uvcf1  21782  lindfrn  21811  mpfrcl  22073  ply1frcl  22293  dfac14lem  23592  flimclslem  23959  lebnumlem3  24940  pmltpclem2  25426  i1fmullem  25671  fta1glem1  26143  fta1blem  26146  dgrcolem1  26248  plydivlem4  26273  plyrem  26282  facth  26283  fta1lem  26284  vieta1lem1  26287  vieta1lem2  26288  vieta1  26289  aalioulem2  26310  geolim3  26316  logcj  26583  argregt0  26587  argimgt0  26589  argimlt0  26590  logneg2  26592  tanarg  26596  logtayl  26637  cxpsqrt  26680  cxpcn3lem  26724  cxpcn3  26725  dcubic2  26821  dcubic  26823  cubic  26826  asinlem  26845  atandmcj  26886  atancj  26887  atanlogsublem  26892  bndatandm  26906  birthdaylem1  26928  basellem4  27061  dchrn0  27227  lgsne0  27312  usgr2trlncl  29843  nmlno0lem  30879  nmlnop0iALT  32081  eldmne0  32715  preimane  32757  prmidl0  33525  constrrtll  33891  cntnevol  34388  signsvtn0  34730  signstfveq0a  34736  signstfveq0  34737  nepss  35916  elima4  35974  dfttc4lem2  36727  heicant  37990  totbndbnd  38124  cdleme3c  40690  cdleme7e  40707  sn-1ne2  42717  sn-0ne2  42852  uvcn0  43001  compne  44885  stoweidlem39  46485  sinnpoly  47351  rrx2vlinest  49229  rrx2linesl  49231  elfvne0  49336  lanrcl  50108  ranrcl  50109  rellan  50110  relran  50111