Theorem simprd 112

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  bi2  128  simprbi  269  simplbda  376  simp2  939  simp3  940  sbh  1699  eldifbd  2985  unssbd  3150  opth  3992  potr  4063  frind  4107  brrelex2  4401  feu  5092  fcnvres  5093  fun11iun  5167  elmpt2cl2  5720  tfrlem1  5946  tfrlemisucfn  5961  tfrlemisucaccv  5962  tfrlemibxssdm  5964  tfrlemibfn  5965  tfrlemi14d  5970  swoer  6157  supelti  6415  supisoti  6423  cardcl  6450  isnumi  6451  cardval3ex  6454  indpi  6532  dfplpq2  6544  ltbtwnnq  6606  enq0tr  6624  nqnq0pi  6628  elnp1st2nd  6666  prcunqu  6675  prnmaxl  6678  prloc  6681  genpcuu  6710  addnqprllem  6717  addlocprlemeq  6723  addlocprlemgt  6724  addlocpr  6726  nqprxx  6736  gtnqex  6740  appdivnq  6753  prmuloclemcalc  6755  prmuloc  6756  mullocprlem  6760  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  recexprlemell  6812  recexprlemelu  6813  recexprlemloc  6821  recexprlempr  6822  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  aptipr  6831  cauappcvgprlemlol  6837  cauappcvgprlemupu  6839  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdrl  6847  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemlol  6860  caucvgprlemupu  6862  caucvgprlemladdfu  6867  caucvgprlem1  6869  caucvgprlem2  6870  caucvgprprlemnjltk  6881  caucvgprprlemnbj  6883  caucvgprprlemlol  6888  caucvgprprlemupu  6890  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  ltsrprg  6924  gt0srpr  6925  recexgt0sr  6950  addgt0sr  6952  mulgt0sr  6954  nnindnn  7059  axcaucvglemcau  7064  apreap  7687  apreim  7703  mulge0  7719  apti  7722  mulap0bbd  7750  lble  8025  nnind  8055  recnz  8440  uzind  8458  eluzadd  8647  eluzsub  8648  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccss2  8967  iccssioo2  8969  iccssico2  8970  elfzolt2  9165  ioom  9269  flqltp1  9281  addmodlteq  9400  expcl2lemap  9488  expap0i  9508  crre  9744  caucvgre  9867  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemoverl  9907  sqrtge0  9919  fimaxre2  10109  climi  10126  climge0  10163  evenelz  10266  4dvdseven  10317  infssuzcldc  10347  gcd0id  10370  gcd1  10378  bezoutlemstep  10386  dvdsgcdb  10402  mulgcd  10405  gcdzeq  10411  dvdsmulgcd  10414  sqgcd  10418  dvdssqlem  10419  bezoutr  10421  lcmval  10445  lcmcllem  10449  lcmgcdlem  10459  lcmdvds  10461  lcmgcdeq  10465  lcmdvdsb  10466  mulgcddvds  10476  rpmulgcd2  10477  qredeu  10479  rpdvds  10481  divgcdcoprm0  10483  isprm3  10500  divgcdodd  10522  coprm  10523  rpexp  10532  sqrt2irr  10541  bj-inf2vnlem1  10765  alsi2d  10793  alsc2d  10795