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  942  simp3  943  sbh  1703  eldifbd  3000  unssbd  3167  opth  4036  potr  4107  frind  4151  brrelex2  4447  funinsn  5024  feu  5149  fcnvres  5150  fun11iun  5230  elmpt2cl2  5794  tfrlem1  6020  tfrlemisucfn  6036  tfrlemisucaccv  6037  tfrlemibxssdm  6039  tfrlemibfn  6040  tfrlemi14d  6045  swoer  6265  elmapssres  6375  mapsspm  6384  pmsspw  6385  mapss  6393  dom0  6499  xpf1o  6505  sbthlemi8  6609  sbthlemi9  6610  supelti  6633  supisoti  6641  djulclb  6683  cardcl  6745  isnumi  6746  cardval3ex  6749  en2eleq  6757  indpi  6837  dfplpq2  6849  ltbtwnnq  6911  enq0tr  6929  nqnq0pi  6933  elnp1st2nd  6971  prcunqu  6980  prnmaxl  6983  prloc  6986  genpcuu  7015  addnqprllem  7022  addlocprlemeq  7028  addlocprlemgt  7029  addlocpr  7031  nqprxx  7041  gtnqex  7045  appdivnq  7058  prmuloclemcalc  7060  prmuloc  7061  mullocprlem  7065  ltprordil  7084  ltnqpri  7089  ltexprlemm  7095  ltexprlemopl  7096  ltexprlemlol  7097  ltexprlemopu  7098  ltexprlemupu  7099  ltexprlemdisj  7101  ltexprlemloc  7102  ltexprlemfl  7104  ltexprlemrl  7105  ltexprlemfu  7106  ltexprlemru  7107  ltexpri  7108  recexprlemell  7117  recexprlemelu  7118  recexprlemloc  7126  recexprlempr  7127  recexprlem1ssl  7128  recexprlem1ssu  7129  recexprlemss1l  7130  aptipr  7136  cauappcvgprlemlol  7142  cauappcvgprlemupu  7144  cauappcvgprlemladdfu  7149  cauappcvgprlemladdfl  7150  cauappcvgprlemladdrl  7152  caucvgprlemnkj  7161  caucvgprlemnbj  7162  caucvgprlemlol  7165  caucvgprlemupu  7167  caucvgprlemladdfu  7172  caucvgprlem1  7174  caucvgprlem2  7175  caucvgprprlemnjltk  7186  caucvgprprlemnbj  7188  caucvgprprlemlol  7193  caucvgprprlemupu  7195  caucvgprprlemexbt  7201  caucvgprprlem1  7204  caucvgprprlem2  7205  ltsrprg  7229  gt0srpr  7230  recexgt0sr  7255  addgt0sr  7257  mulgt0sr  7259  nnindnn  7364  axcaucvglemcau  7369  apreap  7997  apreim  8013  mulge0  8029  apti  8032  mulap0bbd  8060  lble  8335  nnind  8365  recnz  8764  uzind  8782  eluzadd  8971  eluzsub  8972  ixxss1  9246  ixxss2  9247  ixxss12  9248  iccss2  9286  iccssioo2  9288  iccssico2  9289  elfzolt2  9487  ioom  9592  flqltp1  9606  addmodlteq  9725  expcl2lemap  9857  expap0i  9877  hashennnuni  10075  crre  10178  caucvgre  10301  cvg1nlemcau  10304  cvg1nlemres  10305  resqrexlemoverl  10341  sqrtge0  10353  fimaxre2  10543  climi  10560  climge0  10597  isummolemnm  10650  evenelz  10733  4dvdseven  10783  infssuzcldc  10813  gcd0id  10836  gcd1  10844  bezoutlemstep  10852  dvdsgcdb  10868  mulgcd  10871  gcdzeq  10877  dvdsmulgcd  10880  sqgcd  10884  dvdssqlem  10885  bezoutr  10887  lcmval  10911  lcmcllem  10915  lcmgcdlem  10925  lcmdvds  10927  lcmgcdeq  10931  lcmdvdsb  10932  mulgcddvds  10942  rpmulgcd2  10943  qredeu  10945  rpdvds  10947  divgcdcoprm0  10949  isprm3  10966  divgcdodd  10988  coprm  10989  rpexp  10998  sqrt2irr  11007  qdencl  11033  qeqnumdivden  11038  divnumden  11040  divdenle  11041  densq  11048  phimullem  11067  hashgcdeq  11070  bj-inf2vnlem1  11294  alsi2d  11352  alsc2d  11354