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

Theorem necon3i 2606
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 20 . . 3  |-  ( ( A  =  B  ->  C  =  D )  ->  ( A  =  B  ->  C  =  D ) )
32necon3d 2605 . 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 1649    =/= wne 2567
This theorem is referenced by:  xpnz  5251  unixp  5361  inf3lem2  7540  infeq5  7548  cantnflem1  7601  iunfictbso  7951  rankcf  8608  hashfun  11655  s1nz  11714  abssubne0  12075  expnprm  13226  grpn0  14792  gsumval3  15469  pgpfaclem2  15595  isdrng2  15800  gzrngunit  16719  zrngunit  16720  prmirredlem  16728  dfac14lem  17602  flimclslem  17969  lebnumlem3  18941  pmltpclem2  19299  i1fmullem  19539  mpfrcl  19892  fta1glem1  20041  fta1blem  20044  dgrcolem1  20144  plydivlem4  20166  plyrem  20175  facth  20176  fta1lem  20177  vieta1lem1  20180  vieta1lem2  20181  vieta1  20182  aalioulem2  20203  geolim3  20209  logcj  20454  argregt0  20458  argimgt0  20460  argimlt0  20461  logneg2  20463  tanarg  20467  logtayl  20504  cxpsqr  20547  cxpcn3lem  20584  cxpcn3  20585  dcubic2  20637  dcubic  20639  cubic  20642  asinlem  20661  atandmcj  20702  atancj  20703  atanlogsublem  20708  bndatandm  20722  birthdaylem1  20743  basellem4  20819  basellem5  20820  dchrn0  20987  lgsne0  21070  constr3lem2  21586  nmlno0lem  22247  nmlnop0iALT  23451  difneqnul  23950  cntnevol  24535  nepss  25128  totbndbnd  26388  uvcf1  27109  lindfrn  27159  compne  27510  stoweidlem39  27655  cdleme3c  30712  cdleme7e  30729
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 178  df-ne 2569
  Copyright terms: Public domain W3C validator