Theorem simprd 113

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  bi2  129  simprbi  271  simplbda  379  simp2  963  simp3  964  sbh  1730  eldifbd  3047  unssbd  3218  opth  4117  potr  4188  frind  4232  brrelex2  4538  funinsn  5128  feu  5261  fcnvres  5262  fun11iun  5342  elmpocl2  5922  oprssdmm  6021  tfrlem1  6157  tfrlemisucfn  6173  tfrlemisucaccv  6174  tfrlemibxssdm  6176  tfrlemibfn  6177  tfrlemi14d  6182  swoer  6409  elmapssres  6519  mapsspm  6528  pmsspw  6529  mapss  6537  dom0  6683  xpf1o  6689  sbthlemi8  6802  sbthlemi9  6803  supelti  6839  supisoti  6847  djulclb  6890  cardcl  6984  isnumi  6985  cardval3ex  6988  en2eleq  6996  acfun  7008  exmidaclem  7009  indpi  7092  dfplpq2  7104  ltbtwnnq  7166  enq0tr  7184  nqnq0pi  7188  elnp1st2nd  7226  prcunqu  7235  prnmaxl  7238  prloc  7241  genpcuu  7270  addnqprllem  7277  addlocprlemeq  7283  addlocprlemgt  7284  addlocpr  7286  nqprxx  7296  gtnqex  7300  appdivnq  7313  prmuloclemcalc  7315  prmuloc  7316  mullocprlem  7320  ltprordil  7339  ltnqpri  7344  ltexprlemm  7350  ltexprlemopl  7351  ltexprlemlol  7352  ltexprlemopu  7353  ltexprlemupu  7354  ltexprlemdisj  7356  ltexprlemloc  7357  ltexprlemfl  7359  ltexprlemrl  7360  ltexprlemfu  7361  ltexprlemru  7362  ltexpri  7363  recexprlemell  7372  recexprlemelu  7373  recexprlemloc  7381  recexprlempr  7382  recexprlem1ssl  7383  recexprlem1ssu  7384  recexprlemss1l  7385  aptipr  7391  cauappcvgprlemlol  7397  cauappcvgprlemupu  7399  cauappcvgprlemladdfu  7404  cauappcvgprlemladdfl  7405  cauappcvgprlemladdrl  7407  caucvgprlemnkj  7416  caucvgprlemnbj  7417  caucvgprlemlol  7420  caucvgprlemupu  7422  caucvgprlemladdfu  7427  caucvgprlem1  7429  caucvgprlem2  7430  caucvgprprlemnjltk  7441  caucvgprprlemnbj  7443  caucvgprprlemlol  7448  caucvgprprlemupu  7450  caucvgprprlemexbt  7456  caucvgprprlem1  7459  caucvgprprlem2  7460  ltsrprg  7484  gt0srpr  7485  recexgt0sr  7510  addgt0sr  7512  mulgt0sr  7514  nnindnn  7622  axcaucvglemcau  7627  apreap  8261  apreim  8277  mulge0  8293  apti  8296  mulap0bbd  8328  lble  8609  nnind  8640  recnz  9042  uzind  9060  eluzadd  9250  eluzsub  9251  ixxss1  9574  ixxss2  9575  ixxss12  9576  iccss2  9614  iccssioo2  9616  iccssico2  9617  elfzolt2  9820  ioom  9925  flqltp1  9939  addmodlteq  10058  expcl2lemap  10192  expap0i  10212  hashennnuni  10412  crre  10516  caucvgre  10639  cvg1nlemcau  10642  cvg1nlemres  10643  resqrexlemoverl  10679  sqrtge0  10691  fimaxre2  10884  climi  10942  reccn2ap  10968  climge0  10980  isummolemnm  11034  sumpr  11068  fsump1i  11088  fsum00  11117  fsumparts  11125  mertenslemi1  11190  addsin  11294  subsin  11295  addcos  11298  subcos  11299  sinbnd2  11306  cosbnd2  11307  evenelz  11406  4dvdseven  11456  infssuzcldc  11486  gcd0id  11509  gcd1  11517  bezoutlemstep  11525  dvdsgcdb  11541  mulgcd  11544  gcdzeq  11550  dvdsmulgcd  11553  sqgcd  11557  dvdssqlem  11558  bezoutr  11560  lcmval  11584  lcmcllem  11588  lcmgcdlem  11598  lcmdvds  11600  lcmgcdeq  11604  lcmdvdsb  11605  mulgcddvds  11615  rpmulgcd2  11616  qredeu  11618  rpdvds  11620  divgcdcoprm0  11622  isprm3  11639  divgcdodd  11661  coprm  11662  rpexp  11671  sqrt2irr  11680  qdencl  11706  qeqnumdivden  11711  divnumden  11713  divdenle  11714  densq  11721  phimullem  11740  hashgcdeq  11743  ennnfonelemom  11760  ennnfonelemex  11766  ennnfonelemf1  11770  ctiunctlemu1st  11784  ctiunctlemu2nd  11785  inopn  12007  restbasg  12174  ssrest  12188  cntop2  12207  icnpimaex  12216  cnima  12225  lmfss  12249  lmtopcnp  12255  psmet0  12310  psmettri2  12311  blhalf  12391  bdxmet  12484  xmetxpbl  12491  ioo2bl  12523  tgioo  12526  cncfi  12545  rescncf  12548  cdivcncfap  12567  limcimo  12584  cnplimcim  12586  cnplimclemr  12588  cnlimci  12592  limccnpcntop  12594  limccnp2lem  12595  limccnp2cntop  12596  reldvg  12597  dvbsssg  12604  dvfgg  12606  dvaddxxbr  12614  bj-inf2vnlem1  12851  pwf1oexmid  12877  alsi2d  12928  alsc2d  12930