Theorem necon3i 2988

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  difn0  4315  imadisjlnd  6078  xpnz  6150  unixp  6285  inf3lem2  9630  infeq5  9638  cantnflem1  9690  iunfictbso  10193  rankcf  10862  hashfun  14582  hashge3el3dif  14632  abssubne0  15484  expnprm  17080  grpn0  19182  pmtr3ncomlem2  19688  pgpfaclem2  20298  isdrng2  20997  prmidl0  21634  gzrngunit  21739  zringunit  21772  prmirredlem  21778  uvcf1  22098  lindfrn  22127  mpfrcl  22394  ply1frcl  22636  dfac14lem  23936  flimclslem  24303  lebnumlem3  25284  pmltpclem2  25770  i1fmullem  26015  fta1glem1  26486  fta1blem  26489  dgrcolem1  26592  plydivlem4  26617  plyrem  26626  facth  26627  fta1lem  26628  vieta1lem1  26633  vieta1lem2  26634  vieta1  26635  aalioulem2  26660  geolim3  26666  logcj  26934  argregt0  26938  argimgt0  26940  argimlt0  26941  logneg2  26943  tanarg  26947  logtayl  26988  cxpsqrt  27031  cxpcn3lem  27075  cxpcn3  27076  dcubic2  27172  dcubic  27174  cubic  27177  asinlem  27196  atandmcj  27237  atancj  27238  atanlogsublem  27243  bndatandm  27257  birthdaylem1  27279  basellem4  27411  dchrn0  27577  lgsne0  27662  usgr2trlncl  30346  nmlno0lem  31395  nmlnop0iALT  32597  eldmne0  33221  preimane  33263  ricnzr1  33849  psrnzr  34144  constrrtll  34363  cntnevol  34861  signsvtn0  35199  signstfveq0a  35205  signstfveq0  35206  nepss  36483  elima4  36540  dfttc4lem2  37317  heicant  38574  totbndbnd  38724  cdleme3c  41288  cdleme7e  41305  sn-1ne2  43331  sn-0ne2  43458  uvcn0  43607  compne  45424  stoweidlem39  47049  sinnpoly  47941  rrx2vlinest  49853  rrx2linesl  49855  elfvne0  49959  lanrcl  50729  ranrcl  50730  rellan  50731  relran  50732