MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3i Structured version   Visualization version   Unicode version

Theorem necon3i 2667
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
StepHypRef Expression
1 necon3i.1 . . 3  |-  ( A  =  B  ->  C  =  D )
21necon3ai 2660 . 2  |-  ( C  =/=  D  ->  -.  A  =  B )
32neqned 2641 1  |-  ( C  =/=  D  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1454    =/= wne 2632
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 190  df-ne 2634
This theorem is referenced by:  difn0  3835  xpnz  5274  unixp  5387  inf3lem2  8159  infeq5  8167  cantnflem1  8219  iunfictbso  8570  rankcf  9227  hashfun  12641  hashge3el3dif  12674  s1nz  12780  abssubne0  13427  expnprm  14895  grpn0  16746  pmtr3ncomlem2  17163  pgpfaclem2  17763  isdrng2  18033  mpfrcl  18789  ply1frcl  18955  gzrngunit  19081  zringunit  19110  prmirredlem  19112  uvcf1  19398  lindfrn  19427  dfac14lem  20680  flimclslem  21047  lebnumlem3  22039  lebnumlem3OLD  22042  pmltpclem2  22448  i1fmullem  22700  fta1glem1  23164  fta1blem  23167  dgrcolem1  23275  plydivlem4  23297  plyrem  23306  facth  23307  fta1lem  23308  vieta1lem1  23311  vieta1lem2  23312  vieta1  23313  aalioulem2  23337  geolim3  23343  logcj  23603  argregt0  23607  argimgt0  23609  argimlt0  23610  logneg2  23612  tanarg  23616  logtayl  23653  cxpsqrt  23696  cxpcn3lem  23735  cxpcn3  23736  dcubic2  23818  dcubic  23820  cubic  23823  asinlem  23842  atandmcj  23883  atancj  23884  atanlogsublem  23889  bndatandm  23903  birthdaylem1  23925  basellem4  24058  basellem5  24059  dchrn0  24226  lgsne0  24309  constr3lem2  25422  nmlno0lem  26482  nmlnop0iALT  27696  cntnevol  29098  signsvtn0  29507  signstfveq0a  29513  signstfveq0  29514  nepss  30398  elima4  30469  heicant  32019  totbndbnd  32165  cdleme3c  33840  cdleme7e  33857  imadisjlnd  36643  compne  36836  stoweidlem39  37937
  Copyright terms: Public domain W3C validator