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

Theorem pm2.61d1 154
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 153 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  ja  156  pm2.61nii  161  pm2.01d  164  ax10lem2OLD  2027  mo  2304  2mo  2360  mosubopt  4455  funfv  5791  dffv2  5797  fvmptnf  5823  rdgsucmptnf  6688  frsucmptn  6697  mapdom2  7279  frfi  7353  oiexg  7505  wemapwe  7655  r1tr  7703  alephsing  8157  uzin  10519  sumeq2ii  12488  sumrblem  12506  fsumcvg  12507  summolem2a  12510  zsum  12513  fsumcvg2  12522  ptpjpre1  17604  qtopres  17731  fgabs  17912  ptcmplem3  18086  setsmstopn  18509  tngtopn  18692  cnmpt2pc  18954  pcoval2  19042  pcopt  19048  pcopt2  19049  itgle  19702  ibladdlem  19712  iblabslem  19720  iblabs  19721  iblabsr  19722  iblmulc2  19723  ditgneg  19745  nbgra0nb  21442  prodeq2ii  25240  prodrblem  25256  fprodcvg  25257  prodmolem2a  25261  zprod  25264  predpoirr  25473  predfrirr  25474  wl-pm5.74lem  26228  ovoliunnfl  26249  voliunnfl  26251  volsupnfl  26252  itg2addnclem  26257  itg2gt0cn  26261  ibladdnclem  26262  iblabsnclem  26269  iblabsnc  26270  iblmulc2nc  26271  bddiblnc  26276  ftc1anclem7  26287  ftc1anclem8  26288  ftc1anc  26289  n4cyclfrgra  28409  dicvalrelN  31984  dihvalrel  32078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator