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

Theorem necon3i 2644
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 21 . . 3  |-  ( ( A  =  B  ->  C  =  D )  ->  ( A  =  B  ->  C  =  D ) )
32necon3d 2640 . 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 1653    =/= wne 2600
This theorem is referenced by:  xpnz  5293  unixp  5403  inf3lem2  7585  infeq5  7593  cantnflem1  7646  iunfictbso  7996  rankcf  8653  hashfun  11701  s1nz  11760  abssubne0  12121  expnprm  13272  grpn0  14838  gsumval3  15515  pgpfaclem2  15641  isdrng2  15846  gzrngunit  16765  zrngunit  16766  prmirredlem  16774  dfac14lem  17650  flimclslem  18017  lebnumlem3  18989  pmltpclem2  19347  i1fmullem  19587  mpfrcl  19940  fta1glem1  20089  fta1blem  20092  dgrcolem1  20192  plydivlem4  20214  plyrem  20223  facth  20224  fta1lem  20225  vieta1lem1  20228  vieta1lem2  20229  vieta1  20230  aalioulem2  20251  geolim3  20257  logcj  20502  argregt0  20506  argimgt0  20508  argimlt0  20509  logneg2  20511  tanarg  20515  logtayl  20552  cxpsqr  20595  cxpcn3lem  20632  cxpcn3  20633  dcubic2  20685  dcubic  20687  cubic  20690  asinlem  20709  atandmcj  20750  atancj  20751  atanlogsublem  20756  bndatandm  20770  birthdaylem1  20791  basellem4  20867  basellem5  20868  dchrn0  21035  lgsne0  21118  constr3lem2  21634  nmlno0lem  22295  nmlnop0iALT  23499  difneqnul  23998  cntnevol  24583  nepss  25176  elima4  25405  totbndbnd  26499  uvcf1  27219  lindfrn  27269  compne  27620  stoweidlem39  27765  cdleme3c  31028  cdleme7e  31045
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 179  df-ne 2602
  Copyright terms: Public domain W3C validator