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

Theorem necon3i 2674
Description: Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
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 . 2  |-  ( A  =  B  ->  C  =  D )
2 id 22 . . 3  |-  ( ( A  =  B  ->  C  =  D )  ->  ( A  =  B  ->  C  =  D ) )
32necon3d 2670 . 2  |-  ( ( A  =  B  ->  C  =  D )  ->  ( C  =/=  D  ->  A  =/=  B ) )
41, 3ax-mp 5 1  |-  ( C  =/=  D  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    =/= wne 2620
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 2622
This theorem is referenced by:  xpnz  5278  unixp  5391  inf3lem2  7856  infeq5  7864  cantnflem1  7918  cantnflem1OLD  7941  iunfictbso  8305  rankcf  8965  hashge3el3dif  12208  hashfun  12220  s1nz  12318  abssubne0  12825  expnprm  13985  grpn0  15591  pmtr3ncomlem2  16001  gsumval3OLD  16403  pgpfaclem2  16605  isdrng2  16864  mpfrcl  17626  ply1frcl  17775  gzrngunit  17900  zringunit  17936  zrngunit  17937  prmirredlem  17939  prmirredlemOLD  17942  uvcf1  18239  lindfrn  18272  dfac14lem  19212  flimclslem  19579  lebnumlem3  20557  pmltpclem2  20955  i1fmullem  21194  fta1glem1  21659  fta1blem  21662  dgrcolem1  21762  plydivlem4  21784  plyrem  21793  facth  21794  fta1lem  21795  vieta1lem1  21798  vieta1lem2  21799  vieta1  21800  aalioulem2  21821  geolim3  21827  logcj  22077  argregt0  22081  argimgt0  22083  argimlt0  22084  logneg2  22086  tanarg  22090  logtayl  22127  cxpsqr  22170  cxpcn3lem  22207  cxpcn3  22208  dcubic2  22261  dcubic  22263  cubic  22266  asinlem  22285  atandmcj  22326  atancj  22327  atanlogsublem  22332  bndatandm  22346  birthdaylem1  22367  basellem4  22443  basellem5  22444  dchrn0  22611  lgsne0  22694  constr3lem2  23554  nmlno0lem  24215  nmlnop0iALT  25421  difneqnul  25920  cntnevol  26664  signsvtn0  26993  signstfveq0a  26999  signstfveq0  27000  nepss  27396  elima4  27612  heicant  28452  totbndbnd  28714  compne  29722  stoweidlem39  29860  cdleme3c  33970  cdleme7e  33987
  Copyright terms: Public domain W3C validator