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-mp 5  ax-1 6  ax-2 7  ax-ia2 106

This theorem is referenced by:  bi2  129  simprbi  273  simplbda  381  simp2  982  simp3  983  sbh  1749  eldifbd  3078  unssbd  3249  opth  4154  potr  4225  frind  4269  brrelex2  4575  funinsn  5167  feu  5300  fcnvres  5301  fun11iun  5381  elmpocl2  5963  oprssdmm  6062  tfrlem1  6198  tfrlemisucfn  6214  tfrlemisucaccv  6215  tfrlemibxssdm  6217  tfrlemibfn  6218  tfrlemi14d  6223  swoer  6450  elmapssres  6560  mapsspm  6569  pmsspw  6570  mapss  6578  dom0  6725  xpf1o  6731  sbthlemi8  6845  sbthlemi9  6846  supelti  6882  supisoti  6890  djulclb  6933  cardcl  7030  isnumi  7031  cardval3ex  7034  exmidonfinlem  7042  en2eleq  7044  acfun  7056  exmidaclem  7057  ccfunen  7072  indpi  7143  dfplpq2  7155  ltbtwnnq  7217  enq0tr  7235  nqnq0pi  7239  elnp1st2nd  7277  prcunqu  7286  prnmaxl  7289  prloc  7292  genpcuu  7321  addnqprllem  7328  addlocprlemeq  7334  addlocprlemgt  7335  addlocpr  7337  nqprxx  7347  gtnqex  7351  appdivnq  7364  prmuloclemcalc  7366  prmuloc  7367  mullocprlem  7371  ltprordil  7390  ltnqpri  7395  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemfl  7410  ltexprlemrl  7411  ltexprlemfu  7412  ltexprlemru  7413  ltexpri  7414  recexprlemell  7423  recexprlemelu  7424  recexprlemloc  7432  recexprlempr  7433  recexprlem1ssl  7434  recexprlem1ssu  7435  recexprlemss1l  7436  aptipr  7442  cauappcvgprlemlol  7448  cauappcvgprlemupu  7450  cauappcvgprlemladdfu  7455  cauappcvgprlemladdfl  7456  cauappcvgprlemladdrl  7458  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemlol  7471  caucvgprlemupu  7473  caucvgprlemladdfu  7478  caucvgprlem1  7480  caucvgprlem2  7481  caucvgprprlemnjltk  7492  caucvgprprlemnbj  7494  caucvgprprlemlol  7499  caucvgprprlemupu  7501  caucvgprprlemexbt  7507  caucvgprprlem1  7510  caucvgprprlem2  7511  suplocexprlemrl  7518  suplocexprlemru  7520  suplocexprlemdisj  7521  suplocexprlemub  7524  suplocexprlemlub  7525  ltsrprg  7548  gt0srpr  7549  recexgt0sr  7574  addgt0sr  7576  mulgt0sr  7579  map2psrprg  7606  suplocsrlemb  7607  suplocsrlem  7609  nnindnn  7694  axcaucvglemcau  7699  axpre-suploclemres  7702  apreap  8342  apreim  8358  mulge0  8374  apti  8377  mulap0bbd  8414  lble  8698  nnind  8729  recnz  9137  uzind  9155  eluzadd  9347  eluzsub  9348  ixxss1  9680  ixxss2  9681  ixxss12  9682  iccss2  9720  iccssioo2  9722  iccssico2  9723  elfzolt2  9926  ioom  10031  flqltp1  10045  addmodlteq  10164  expcl2lemap  10298  expap0i  10318  hashennnuni  10518  crre  10622  caucvgre  10746  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemoverl  10786  sqrtge0  10798  fimaxre2  10991  climi  11049  reccn2ap  11075  climge0  11087  isummolemnm  11141  sumpr  11175  fsump1i  11195  fsum00  11224  fsumparts  11232  mertenslemi1  11297  addsin  11438  subsin  11439  addcos  11442  subcos  11443  sinbnd2  11450  cosbnd2  11451  evenelz  11553  4dvdseven  11603  infssuzcldc  11633  gcd0id  11656  gcd1  11664  bezoutlemstep  11674  dvdsgcdb  11690  mulgcd  11693  gcdzeq  11699  dvdsmulgcd  11702  sqgcd  11706  dvdssqlem  11707  bezoutr  11709  lcmval  11733  lcmcllem  11737  lcmgcdlem  11747  lcmdvds  11749  lcmgcdeq  11753  lcmdvdsb  11754  mulgcddvds  11764  rpmulgcd2  11765  qredeu  11767  rpdvds  11769  divgcdcoprm0  11771  isprm3  11788  divgcdodd  11810  coprm  11811  rpexp  11820  sqrt2irr  11829  qdencl  11856  qeqnumdivden  11861  divnumden  11863  divdenle  11864  densq  11871  phimullem  11890  hashgcdeq  11893  ennnfonelemom  11910  ennnfonelemex  11916  ennnfonelemf1  11920  ctiunctlemu1st  11936  ctiunctlemu2nd  11937  inopn  12159  restbasg  12326  ssrest  12340  cntop2  12360  icnpimaex  12369  cnima  12378  lmfss  12402  lmtopcnp  12408  txhmeo  12477  txswaphmeo  12479  psmet0  12485  psmettri2  12486  blhalf  12566  bdxmet  12659  xmetxpbl  12666  ioo2bl  12701  tgioo  12704  cncfi  12723  rescncf  12726  cdivcncfap  12745  cnopnap  12752  dedekindeulemeu  12758  dedekindicclemeu  12767  ivthinclemum  12771  ivthinclemlopn  12772  ivthinclemuopn  12774  ivthinclemdisj  12776  ivthdec  12780  limcimo  12792  cnplimcim  12794  cnplimclemr  12796  cnlimci  12800  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  limccoap  12805  reldvg  12806  dvbsssg  12813  dvfgg  12815  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  sin0pilem1  12851  sin0pilem2  12852  tanrpcl  12907  tangtx  12908  bj-inf2vnlem1  13157  pwf1oexmid  13183  subctctexmid  13185  taupi  13228  alsi2d  13237  alsc2d  13239