Theorem necon3i 2987

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

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

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 2956

This theorem is used by:  difn0  4315  imadisjlnd  6077  xpnz  6151  unixp  6280  inf3lem2  9608  infeq5  9616  cantnflem1  9668  iunfictbso  10117  rankcf  10786  hashfun  14502  hashge3el3dif  14552  abssubne0  15404  expnprm  16994  grpn0  19095  pmtr3ncomlem2  19601  pgpfaclem2  20211  isdrng2  20906  prmidl0  21541  gzrngunit  21646  zringunit  21679  prmirredlem  21685  uvcf1  22005  lindfrn  22034  mpfrcl  22301  ply1frcl  22543  dfac14lem  23843  flimclslem  24210  lebnumlem3  25191  pmltpclem2  25677  i1fmullem  25922  fta1glem1  26393  fta1blem  26396  dgrcolem1  26499  plydivlem4  26526  plyrem  26535  facth  26536  fta1lem  26537  vieta1lem1  26542  vieta1lem2  26543  vieta1  26544  aalioulem2  26569  geolim3  26575  logcj  26843  argregt0  26847  argimgt0  26849  argimlt0  26850  logneg2  26852  tanarg  26856  logtayl  26897  cxpsqrt  26940  cxpcn3lem  26984  cxpcn3  26985  dcubic2  27081  dcubic  27083  cubic  27086  asinlem  27105  atandmcj  27146  atancj  27147  atanlogsublem  27152  bndatandm  27166  birthdaylem1  27188  basellem4  27320  dchrn0  27486  lgsne0  27571  usgr2trlncl  30225  nmlno0lem  31274  nmlnop0iALT  32476  eldmne0  33100  preimane  33142  ricnzr1  33728  psrnzr  34022  constrrtll  34241  cntnevol  34739  signsvtn0  35078  signstfveq0a  35084  signstfveq0  35085  nepss  36297  elima4  36355  dfttc4lem2  37148  heicant  38404  totbndbnd  38539  cdleme3c  41103  cdleme7e  41120  sn-1ne2  43146  sn-0ne2  43281  uvcn0  43424  compne  45264  stoweidlem39  46867  sinnpoly  47759  rrx2vlinest  49671  rrx2linesl  49673  elfvne0  49777  lanrcl  50547  ranrcl  50548  rellan  50549  relran  50550