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

Theorem pm2.61d1 159
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 11 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
41, 3pm2.61d 158 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  ja  161  pm2.61nii  166  pm2.01d  169  moOLD  2308  moexex  2352  2mo  2362  2moOLD  2363  mosubopt  4586  funfv  5755  dffv2  5761  fvmptnf  5788  rdgsucmptnf  6881  frsucmptn  6890  mapdom2  7478  frfi  7553  oiexg  7745  wemapwe  7924  wemapweOLD  7925  r1tr  7979  alephsing  8441  uzin  10889  sumeq2ii  13166  sumrblem  13184  fsumcvg  13185  summolem2a  13188  fsumcvg2  13200  ptpjpre1  19103  qtopres  19230  fgabs  19411  ptcmplem3  19585  setsmstopn  20012  tngtopn  20195  cnmpt2pc  20459  pcoval2  20547  pcopt  20553  pcopt2  20554  itgle  21246  ibladdlem  21256  iblabslem  21264  iblabs  21265  iblabsr  21266  iblmulc2  21267  ditgneg  21291  nbgra0nb  23275  prodeq2ii  27355  prodrblem  27371  fprodcvg  27372  prodmolem2a  27376  zprod  27379  predpoirr  27587  predfrirr  27588  ovoliunnfl  28358  voliunnfl  28360  volsupnfl  28361  itg2addnclem  28368  itg2gt0cn  28372  ibladdnclem  28373  iblabsnclem  28380  iblabsnc  28381  iblmulc2nc  28382  bddiblnc  28387  ftc1anclem7  28398  ftc1anclem8  28399  ftc1anc  28400  n4cyclfrgra  30535  ldepspr  30848  dicvalrelN  34552  dihvalrel  34646
  Copyright terms: Public domain W3C validator