Theorem necon3i 2683

Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
necon3i.1	|- ( A = B -> C = D )

Assertion

Ref	Expression
necon3i	|- ( C =/= D -> A =/= B )

Proof of Theorem necon3i

Step	Hyp	Ref	Expression
1		necon3i.1	. . 3 |- ( A = B -> C = D )
2	1	necon3ai 2671	. 2 |- ( C =/= D -> -. A = B )
3	2	neqned 2646	1 |- ( C =/= D -> A =/= B )

Syntax hints:   -> wi 4   = wceq 1383   =/= wne 2638

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 185  df-ne 2640

This theorem is referenced by:  xpnz  5416  unixp  5530  inf3lem2  8049  infeq5  8057  cantnflem1  8111  cantnflem1OLD  8134  iunfictbso  8498  rankcf  9158  hashfun  12477  hashge3el3dif  12506  s1nz  12600  abssubne0  13131  expnprm  14403  grpn0  16061  pmtr3ncomlem2  16478  gsumval3OLD  16887  pgpfaclem2  17112  isdrng2  17385  mpfrcl  18166  ply1frcl  18334  gzrngunit  18462  zringunit  18498  zrngunit  18499  prmirredlem  18501  prmirredlemOLD  18504  uvcf1  18801  lindfrn  18834  dfac14lem  20096  flimclslem  20463  lebnumlem3  21441  pmltpclem2  21839  i1fmullem  22079  fta1glem1  22544  fta1blem  22547  dgrcolem1  22648  plydivlem4  22670  plyrem  22679  facth  22680  fta1lem  22681  vieta1lem1  22684  vieta1lem2  22685  vieta1  22686  aalioulem2  22707  geolim3  22713  logcj  22969  argregt0  22973  argimgt0  22975  argimlt0  22976  logneg2  22978  tanarg  22982  logtayl  23019  cxpsqrt  23062  cxpcn3lem  23099  cxpcn3  23100  dcubic2  23153  dcubic  23155  cubic  23158  asinlem  23177  atandmcj  23218  atancj  23219  atanlogsublem  23224  bndatandm  23238  birthdaylem1  23259  basellem4  23335  basellem5  23336  dchrn0  23503  lgsne0  23586  constr3lem2  24624  nmlno0lem  25686  nmlnop0iALT  26892  difneqnul  27393  cntnevol  28177  signsvtn0  28505  signstfveq0a  28511  signstfveq0  28512  nepss  29073  elima4  29185  heicant  30025  totbndbnd  30261  compne  31303  stoweidlem39  31775  cdleme3c  35830  cdleme7e  35847  imadisjlnd  37777