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  1877  mo  2165  2mo  2221  mosubopt  4264  funfv  5586  dffv2  5592  fvmptnf  5617  rdgsucmptnf  6442  frsucmptn  6451  mapdom2  7032  frfi  7102  oiexg  7250  wemapwe  7400  r1tr  7448  alephsing  7902  uzin  10260  sumeq2ii  12166  sumrblem  12184  fsumcvg  12185  summolem2a  12188  zsum  12191  fsumcvg2  12200  ptpjpre1  17266  qtopres  17389  fgabs  17574  ptcmplem3  17748  setsmstopn  18024  tngtopn  18166  cnmpt2pc  18426  pcoval2  18514  pcopt  18520  pcopt2  18521  itgle  19164  ibladdlem  19174  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  ditgneg  19207  predpoirr  24197  predfrirr  24198  wl-pm5.74lem  24917  nbgra0nb  28144  a12study4  29117  ax9lem15  29154  dicvalrelN  31375  dihvalrel  31469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator