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

Theorem necon3i 2640
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 2636 . 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 1362    =/= wne 2596
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 2598
This theorem is referenced by:  xpnz  5245  unixp  5358  inf3lem2  7823  infeq5  7831  cantnflem1  7885  cantnflem1OLD  7908  iunfictbso  8272  rankcf  8931  hashge3el3dif  12170  hashfun  12182  s1nz  12280  abssubne0  12787  expnprm  13946  grpn0  15549  pmtr3ncomlem2  15959  gsumval3OLD  16361  pgpfaclem2  16556  isdrng2  16765  gzrngunit  17721  zringunit  17755  zrngunit  17756  prmirredlem  17758  prmirredlemOLD  17761  uvcf1  18058  lindfrn  18091  dfac14lem  19031  flimclslem  19398  lebnumlem3  20376  pmltpclem2  20774  i1fmullem  21013  mpfrcl  21369  fta1glem1  21521  fta1blem  21524  dgrcolem1  21624  plydivlem4  21646  plyrem  21655  facth  21656  fta1lem  21657  vieta1lem1  21660  vieta1lem2  21661  vieta1  21662  aalioulem2  21683  geolim3  21689  logcj  21939  argregt0  21943  argimgt0  21945  argimlt0  21946  logneg2  21948  tanarg  21952  logtayl  21989  cxpsqr  22032  cxpcn3lem  22069  cxpcn3  22070  dcubic2  22123  dcubic  22125  cubic  22128  asinlem  22147  atandmcj  22188  atancj  22189  atanlogsublem  22194  bndatandm  22208  birthdaylem1  22229  basellem4  22305  basellem5  22306  dchrn0  22473  lgsne0  22556  constr3lem2  23354  nmlno0lem  24015  nmlnop0iALT  25221  difneqnul  25721  cntnevol  26495  signsvtn0  26818  signstfveq0a  26824  signstfveq0  26825  nepss  27220  elima4  27436  heicant  28267  totbndbnd  28529  compne  29538  stoweidlem39  29677  cdleme3c  33444  cdleme7e  33461
  Copyright terms: Public domain W3C validator