Theorem necon3i 2707

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 2695	. 2 |- ( C =/= D -> -. A = B )
3	2	neqned 2670	1 |- ( C =/= D -> A =/= B )

Syntax hints:   -> wi 4   = wceq 1379   =/= wne 2662

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 2664

This theorem is referenced by:  xpnz  5426  unixp  5540  inf3lem2  8046  infeq5  8054  cantnflem1  8108  cantnflem1OLD  8131  iunfictbso  8495  rankcf  9155  hashfun  12461  hashge3el3dif  12490  s1nz  12581  abssubne0  13112  expnprm  14280  grpn0  15892  pmtr3ncomlem2  16305  gsumval3OLD  16711  pgpfaclem2  16935  isdrng2  17206  mpfrcl  17986  ply1frcl  18154  gzrngunit  18279  zringunit  18315  zrngunit  18316  prmirredlem  18318  prmirredlemOLD  18321  uvcf1  18618  lindfrn  18651  dfac14lem  19881  flimclslem  20248  lebnumlem3  21226  pmltpclem2  21624  i1fmullem  21864  fta1glem1  22329  fta1blem  22332  dgrcolem1  22432  plydivlem4  22454  plyrem  22463  facth  22464  fta1lem  22465  vieta1lem1  22468  vieta1lem2  22469  vieta1  22470  aalioulem2  22491  geolim3  22497  logcj  22747  argregt0  22751  argimgt0  22753  argimlt0  22754  logneg2  22756  tanarg  22760  logtayl  22797  cxpsqrt  22840  cxpcn3lem  22877  cxpcn3  22878  dcubic2  22931  dcubic  22933  cubic  22936  asinlem  22955  atandmcj  22996  atancj  22997  atanlogsublem  23002  bndatandm  23016  birthdaylem1  23037  basellem4  23113  basellem5  23114  dchrn0  23281  lgsne0  23364  constr3lem2  24350  nmlno0lem  25412  nmlnop0iALT  26618  difneqnul  27117  cntnevol  27867  signsvtn0  28195  signstfveq0a  28201  signstfveq0  28202  nepss  28598  elima4  28814  heicant  29654  totbndbnd  29916  compne  30955  stoweidlem39  31367  cdleme3c  35044  cdleme7e  35061