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

Theorem pm2.61d1 151
Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
Hypotheses
Ref Expression
pm2.61d1.1  |-  ( ph  ->  ( ps  ->  ch ) )
pm2.61d1.2  |-  ( -. 
ps  ->  ch )
Assertion
Ref Expression
pm2.61d1  |-  ( ph  ->  ch )

Proof of Theorem pm2.61d1
StepHypRef Expression
1 pm2.61d1.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 pm2.61d1.2 . . 3  |-  ( -. 
ps  ->  ch )
32a1i 10 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
41, 3pm2.61d 150 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  ja  153  pm2.61nii  158  pm2.01d  161  ax10lem2  1890  mo  2178  2mo  2234  mosubopt  4280  funfv  5602  dffv2  5608  fvmptnf  5633  rdgsucmptnf  6458  frsucmptn  6467  mapdom2  7048  frfi  7118  oiexg  7266  wemapwe  7416  r1tr  7464  alephsing  7918  uzin  10276  sumeq2ii  12182  sumrblem  12200  fsumcvg  12201  summolem2a  12204  zsum  12207  fsumcvg2  12216  ptpjpre1  17282  qtopres  17405  fgabs  17590  ptcmplem3  17764  setsmstopn  18040  tngtopn  18182  cnmpt2pc  18442  pcoval2  18530  pcopt  18536  pcopt2  18537  itgle  19180  ibladdlem  19190  iblabslem  19198  iblabs  19199  iblabsr  19200  iblmulc2  19201  ditgneg  19223  cprodeq2ii  24135  prodrblem  24152  fprodcvg  24153  prodmolem2a  24157  zprod  24160  predpoirr  24268  predfrirr  24269  wl-pm5.74lem  24989  ovoliunnfl  25001  itg2gt0cn  25006  ibladdnclem  25007  iblabsnclem  25014  iblabsnc  25015  iblmulc2nc  25016  bddiblnc  25021  nbgra0nb  28278  n4cyclfrgra  28440  a12study4  29739  ax9lem15  29776  dicvalrelN  31997  dihvalrel  32091
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator