Theorem necon3i 2826

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

Syntax hints:   → wi 4   = wceq 1483   ≠ wne 2794

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 2795

This theorem is referenced by:  difn0  3943  xpnz  5553  unixp  5668  inf3lem2  8526  infeq5  8534  cantnflem1  8586  iunfictbso  8937  rankcf  9599  hashfun  13224  hashge3el3dif  13268  s1nzOLD  13387  abssubne0  14056  expnprm  15606  grpn0  17454  pmtr3ncomlem2  17894  pgpfaclem2  18481  isdrng2  18757  mpfrcl  19518  ply1frcl  19683  gzrngunit  19812  zringunit  19836  prmirredlem  19841  uvcf1  20131  lindfrn  20160  dfac14lem  21420  flimclslem  21788  lebnumlem3  22762  pmltpclem2  23218  i1fmullem  23461  fta1glem1  23925  fta1blem  23928  dgrcolem1  24029  plydivlem4  24051  plyrem  24060  facth  24061  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  vieta1  24067  aalioulem2  24088  geolim3  24094  logcj  24352  argregt0  24356  argimgt0  24358  argimlt0  24359  logneg2  24361  tanarg  24365  logtayl  24406  cxpsqrt  24449  cxpcn3lem  24488  cxpcn3  24489  dcubic2  24571  dcubic  24573  cubic  24576  asinlem  24595  atandmcj  24636  atancj  24637  atanlogsublem  24642  bndatandm  24656  birthdaylem1  24678  basellem4  24810  basellem5  24811  dchrn0  24975  lgsne0  25060  usgr2trlncl  26656  nmlno0lem  27648  nmlnop0iALT  28854  cntnevol  30291  signsvtn0  30647  signstfveq0a  30653  signstfveq0  30654  nepss  31599  elima4  31679  heicant  33444  totbndbnd  33588  cdleme3c  35517  cdleme7e  35534  imadisjlnd  38459  compne  38643  compneOLD  38644  stoweidlem39  40256