Theorem necon3i 2975

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

Syntax hints:   → wi 4   = wceq 1631   ≠ wne 2943

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 197  df-ne 2944

This theorem is referenced by:  difn0  4091  xpnz  5693  unixp  5811  inf3lem2  8694  infeq5  8702  cantnflem1  8754  iunfictbso  9141  rankcf  9805  hashfun  13426  hashge3el3dif  13470  abssubne0  14264  expnprm  15813  grpn0  17662  pmtr3ncomlem2  18101  pgpfaclem2  18689  isdrng2  18967  mpfrcl  19733  ply1frcl  19898  gzrngunit  20027  zringunit  20051  prmirredlem  20056  uvcf1  20348  lindfrn  20377  dfac14lem  21641  flimclslem  22008  lebnumlem3  22982  pmltpclem2  23437  i1fmullem  23681  fta1glem1  24145  fta1blem  24148  dgrcolem1  24249  plydivlem4  24271  plyrem  24280  facth  24281  fta1lem  24282  vieta1lem1  24285  vieta1lem2  24286  vieta1  24287  aalioulem2  24308  geolim3  24314  logcj  24573  argregt0  24577  argimgt0  24579  argimlt0  24580  logneg2  24582  tanarg  24586  logtayl  24627  cxpsqrt  24670  cxpcn3lem  24709  cxpcn3  24710  dcubic2  24792  dcubic  24794  cubic  24797  asinlem  24816  atandmcj  24857  atancj  24858  atanlogsublem  24863  bndatandm  24877  birthdaylem1  24899  basellem4  25031  basellem5  25032  dchrn0  25196  lgsne0  25281  usgr2trlncl  26891  nmlno0lem  27988  nmlnop0iALT  29194  cntnevol  30631  signsvtn0  30987  signstfveq0a  30993  signstfveq0  30994  nepss  31937  elima4  32015  heicant  33776  totbndbnd  33918  cdleme3c  36038  cdleme7e  36055  imadisjlnd  38983  compne  39167  compneOLD  39168  stoweidlem39  40768