Theorem necon3i 2957

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

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

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 2926

This theorem is referenced by:  difn0  4318  imadisjlnd  6032  xpnz  6108  unixp  6230  inf3lem2  9525  infeq5  9533  cantnflem1  9585  iunfictbso  10008  rankcf  10671  hashfun  14344  hashge3el3dif  14394  abssubne0  15224  expnprm  16814  grpn0  18850  pmtr3ncomlem2  19353  pgpfaclem2  19963  isdrng2  20628  gzrngunit  21340  zringunit  21373  prmirredlem  21379  uvcf1  21699  lindfrn  21728  mpfrcl  21990  ply1frcl  22203  dfac14lem  23502  flimclslem  23869  lebnumlem3  24860  pmltpclem2  25348  i1fmullem  25593  fta1glem1  26071  fta1blem  26074  dgrcolem1  26177  plydivlem4  26202  plyrem  26211  facth  26212  fta1lem  26213  vieta1lem1  26216  vieta1lem2  26217  vieta1  26218  aalioulem2  26239  geolim3  26245  logcj  26513  argregt0  26517  argimgt0  26519  argimlt0  26520  logneg2  26522  tanarg  26526  logtayl  26567  cxpsqrt  26610  cxpcn3lem  26655  cxpcn3  26656  dcubic2  26752  dcubic  26754  cubic  26757  asinlem  26776  atandmcj  26817  atancj  26818  atanlogsublem  26823  bndatandm  26837  birthdaylem1  26859  basellem4  26992  dchrn0  27159  lgsne0  27244  usgr2trlncl  29705  nmlno0lem  30737  nmlnop0iALT  31939  eldmne0  32570  preimane  32613  prmidl0  33387  constrrtll  33698  cntnevol  34195  signsvtn0  34538  signstfveq0a  34544  signstfveq0  34545  nepss  35691  elima4  35749  heicant  37635  totbndbnd  37769  cdleme3c  40209  cdleme7e  40226  sn-1ne2  42238  sn-0ne2  42379  uvcn0  42515  compne  44414  stoweidlem39  46020  sinnpoly  46875  rrx2vlinest  48726  rrx2linesl  48728  elfvne0  48833  lanrcl  49606  ranrcl  49607  rellan  49608  relran  49609