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

Theorem necon3i 2498
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 19 . . 3  |-  ( ( A  =  B  ->  C  =  D )  ->  ( A  =  B  ->  C  =  D ) )
32necon3d 2497 . 2  |-  ( ( A  =  B  ->  C  =  D )  ->  ( C  =/=  D  ->  A  =/=  B ) )
41, 3ax-mp 8 1  |-  ( C  =/=  D  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  xpnz  5115  unixp  5221  inf3lem2  7346  infeq5  7354  cantnflem1  7407  iunfictbso  7757  rankcf  8415  hashfun  11405  s1nz  11461  abssubne0  11816  expnprm  12966  grpn0  14530  gsumval3  15207  pgpfaclem2  15333  isdrng2  15538  gzrngunit  16453  zrngunit  16454  prmirredlem  16462  dfac14lem  17327  flimclslem  17695  lebnumlem3  18477  pmltpclem2  18825  i1fmullem  19065  mpfrcl  19418  fta1glem1  19567  fta1blem  19570  dgrcolem1  19670  plydivlem4  19692  plyrem  19701  facth  19702  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  vieta1  19708  aalioulem2  19729  geolim3  19735  logcj  19976  argregt0  19980  argimgt0  19982  argimlt0  19983  logneg2  19985  tanarg  19986  logtayl  20023  cxpsqr  20066  cxpcn3lem  20103  cxpcn3  20104  dcubic2  20156  dcubic  20158  cubic  20161  asinlem  20180  atandmcj  20221  atancj  20222  atanlogsublem  20227  bndatandm  20241  birthdaylem1  20262  basellem4  20337  basellem5  20338  dchrn0  20505  lgsne0  20588  nmlno0lem  21387  nmlnop0iALT  22591  difneqnul  23143  cntnevol  23191  nepss  24087  hdrmp  25809  totbndbnd  26616  uvcf1  27344  lindfrn  27394  compne  27745  stoweidlem39  27891  constr3lem2  28392  cdleme3c  31041  cdleme7e  31058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2461
  Copyright terms: Public domain W3C validator