Theorem simprd 107

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

Ref	Expression
simprd.1	|- ( ph -> ( ps /\ ch ) )

Assertion

Ref	Expression
simprd	|- ( ph -> ch )

Proof of Theorem simprd

Step	Hyp	Ref	Expression
1		simprd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpr 103	. 2 |- ( ( ps /\ ch ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100

This theorem is referenced by:  bi2  121  simprbi  260  simplbda  366  simp2  905  simp3  906  sbh  1659  eldifbd  2930  unssbd  3121  opth  3974  potr  4045  frind  4089  brrelex2  4383  feu  5072  fcnvres  5073  fun11iun  5147  elmpt2cl2  5700  tfrlem1  5923  tfrlemisucfn  5938  tfrlemisucaccv  5939  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemi14d  5947  swoer  6134  cardcl  6361  isnumi  6362  cardval3ex  6365  indpi  6440  dfplpq2  6452  ltbtwnnq  6514  enq0tr  6532  nqnq0pi  6536  elnp1st2nd  6574  prcunqu  6583  prnmaxl  6586  prloc  6589  genpcuu  6618  addnqprllem  6625  addlocprlemeq  6631  addlocprlemgt  6632  addlocpr  6634  nqprxx  6644  gtnqex  6648  appdivnq  6661  prmuloclemcalc  6663  prmuloc  6664  mullocprlem  6668  ltprordil  6687  ltnqpri  6692  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemlol  6700  ltexprlemopu  6701  ltexprlemupu  6702  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  ltexpri  6711  recexprlemell  6720  recexprlemelu  6721  recexprlemloc  6729  recexprlempr  6730  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1l  6733  aptipr  6739  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdrl  6755  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprlemladdfu  6775  caucvgprlem1  6777  caucvgprlem2  6778  caucvgprprlemnjltk  6789  caucvgprprlemnbj  6791  caucvgprprlemlol  6796  caucvgprprlemupu  6798  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  ltsrprg  6832  gt0srpr  6833  recexgt0sr  6858  addgt0sr  6860  mulgt0sr  6862  nnindnn  6967  axcaucvglemcau  6972  apreap  7578  apreim  7594  mulge0  7610  apti  7613  mulap0bbd  7641  nnind  7930  recnz  8333  uzind  8349  eluzadd  8501  eluzsub  8502  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  iccssioo2  8815  iccssico2  8816  elfzolt2  9012  flqltp1  9121  expcl2lemap  9267  expap0i  9287  crre  9457  caucvgre  9580  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemoverl  9619  sqrtge0  9631  climi  9808  climge0  9845  sqrt2irr  9878  bj-inf2vnlem1  10095  alsi2d  10121  alsc2d  10123