Theorem simpld 105

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
simpld	|- ( ph -> ps )

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpl 102	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem is referenced by:  bi1  111  simplbi  259  simprbda  365  simp1  904  eldifad  2929  unssad  3120  opth1  3973  opth  3974  0nelop  3985  epelg  4027  poirr  4044  brrelex  4382  asymref  4710  soirri  4719  sotri  4720  fcnvres  5073  fun11iun  5147  elmpt2cl1  5699  f1od  5703  f1o2d  5705  smoiso  5917  tfrlem1  5923  swoer  6134  ecopovtrn  6203  ecopovtrng  6206  en1uniel  6284  dfplpq2  6452  ltbtwnnqq  6513  enq0tr  6532  elnp1st2nd  6574  prcdnql  6582  prnminu  6587  prloc  6589  genpcdl  6617  addnqprulem  6626  addlocprlemlt  6629  addlocprlemgt  6632  addlocprlem  6633  addlocpr  6634  nqprxx  6644  ltnqex  6647  addnqprlemfl  6657  addnqprlemfu  6658  appdivnq  6661  prmuloclemcalc  6663  prmuloc  6664  mullocprlem  6668  mulnqprlemfl  6673  mulnqprlemfu  6674  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  lteupri  6715  ltaprlem  6716  recexprlemell  6720  recexprlemelu  6721  recexprlemloc  6729  recexprlempr  6730  recexprlem1ssl  6731  recexprlem1ssu  6732  recexprlemss1u  6734  aptipr  6739  cauappcvgprlemm  6743  cauappcvgprlemlol  6745  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlem1  6757  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemlol  6768  caucvgprlemladdfu  6775  caucvgprprlemloccalc  6782  caucvgprprlemnkltj  6787  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemlol  6796  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  ltsrprg  6832  caucvgsrlemasr  6874  axcaucvglemcau  6972  apreap  7578  apreim  7594  msqge0  7607  mulge0  7610  apti  7613  mulap0bad  7640  divadddivap  7703  recnz  8333  lbzbi  8551  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  iccssioo2  8815  iccssico2  8816  elfzole1  9011  flqle  9120  flqltnz  9129  expclzap  9280  recl  9453  cvg1nlemcau  9583  cvg1nlemres  9584  resqrtth  9629  climcl  9803  sqrt2irr  9878  alsi1d  10120  alsc1d  10122