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

Theorem necon3i 2485
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 2484 . 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 1623    =/= wne 2446
This theorem is referenced by:  xpnz  5099  unixp  5205  inf3lem2  7330  infeq5  7338  cantnflem1  7391  iunfictbso  7741  rankcf  8399  hashfun  11389  s1nz  11445  abssubne0  11800  expnprm  12950  grpn0  14514  gsumval3  15191  pgpfaclem2  15317  isdrng2  15522  gzrngunit  16437  zrngunit  16438  prmirredlem  16446  dfac14lem  17311  flimclslem  17679  lebnumlem3  18461  pmltpclem2  18809  i1fmullem  19049  mpfrcl  19402  fta1glem1  19551  fta1blem  19554  dgrcolem1  19654  plydivlem4  19676  plyrem  19685  facth  19686  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  aalioulem2  19713  geolim3  19719  logcj  19960  argregt0  19964  argimgt0  19966  argimlt0  19967  logneg2  19969  tanarg  19970  logtayl  20007  cxpsqr  20050  cxpcn3lem  20087  cxpcn3  20088  dcubic2  20140  dcubic  20142  cubic  20145  asinlem  20164  atandmcj  20205  atancj  20206  atanlogsublem  20211  bndatandm  20225  birthdaylem1  20246  basellem4  20321  basellem5  20322  dchrn0  20489  lgsne0  20572  nmlno0lem  21371  nmlnop0iALT  22575  difneqnul  23127  cntnevol  23175  nepss  24072  funpartfv  24483  hdrmp  25706  totbndbnd  26513  uvcf1  27241  lindfrn  27291  compne  27642  stoweidlem39  27788  cdleme3c  30419  cdleme7e  30436
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 2448
  Copyright terms: Public domain W3C validator