Theorem simpld 110

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 107	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  bi1  116  simplbi  268  simprbda  375  simp1  938  eldifad  2984  unssad  3149  opth1  3991  opth  3992  0nelop  4003  epelg  4045  poirr  4062  brrelex  4400  asymref  4730  soirri  4739  sotri  4740  fcnvres  5093  fun11iun  5167  elmpt2cl1  5719  f1od  5723  f1o2d  5725  smoiso  5940  tfrlem1  5946  swoer  6157  ecopovtrn  6226  ecopovtrng  6229  en1uniel  6307  supelti  6415  supsnti  6418  supisoti  6423  dfplpq2  6544  ltbtwnnqq  6605  enq0tr  6624  elnp1st2nd  6666  prcdnql  6674  prnminu  6679  prloc  6681  genpcdl  6709  addnqprulem  6718  addlocprlemlt  6721  addlocprlemgt  6724  addlocprlem  6725  addlocpr  6726  nqprxx  6736  ltnqex  6739  addnqprlemfl  6749  addnqprlemfu  6750  appdivnq  6753  prmuloclemcalc  6755  prmuloc  6756  mullocprlem  6760  mulnqprlemfl  6765  mulnqprlemfu  6766  ltprordil  6779  ltnqpri  6784  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  ltexpri  6803  lteupri  6807  ltaprlem  6808  recexprlemell  6812  recexprlemelu  6813  recexprlemloc  6821  recexprlempr  6822  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1u  6826  aptipr  6831  cauappcvgprlemm  6835  cauappcvgprlemlol  6837  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlem1  6849  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemlol  6860  caucvgprlemladdfu  6867  caucvgprprlemloccalc  6874  caucvgprprlemnkltj  6879  caucvgprprlemnbj  6883  caucvgprprlemml  6884  caucvgprprlemlol  6888  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  ltsrprg  6924  caucvgsrlemasr  6966  axcaucvglemcau  7064  negf1o  7486  apreap  7687  apreim  7703  msqge0  7716  mulge0  7719  apti  7722  mulap0bad  7749  divadddivap  7815  recnz  8440  lbzbi  8701  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccss2  8967  iccssioo2  8969  iccssico2  8970  elfzole1  9164  ioom  9269  flqle  9280  flqltnz  9289  addmodlteq  9400  expclzap  9501  recl  9740  cvg1nlemcau  9870  cvg1nlemres  9871  resqrtth  9917  fimaxre2  10109  climcl  10121  divgcdz  10363  divgcdnn  10366  gcdaddm  10375  bezoutlemstep  10386  dvdsgcdb  10402  dfgcd2  10403  mulgcd  10405  gcdzeq  10411  dvdsmulgcd  10414  sqgcd  10418  bezoutr  10421  lcmval  10445  lcmcllem  10449  gcddvdslcm  10455  lcmgcdlem  10459  lcmgcd  10460  lcmgcdeq  10465  lcmdvdsb  10466  mulgcddvds  10476  rpmulgcd2  10477  qredeu  10479  rpdvds  10481  isprm3  10500  divgcdodd  10522  coprm  10523  rpexp  10532  sqrt2irr  10541  alsi1d  10792  alsc1d  10794