Theorem simprd 114

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  biimpr  130  simprbi  275  simplbda  384  simprld  530  simprrd  532  simp2  998  simp3  999  sbh  1776  eldifbd  3142  unssbd  3314  opth  4238  potr  4309  frind  4353  brrelex2  4668  funinsn  5266  feu  5399  fcnvres  5400  fun11iun  5483  elmpocl2  6071  oprssdmm  6172  tfrlem1  6309  tfrlemisucfn  6325  tfrlemisucaccv  6326  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemi14d  6334  swoer  6563  elmapssres  6673  mapsspm  6682  pmsspw  6683  mapss  6691  dom0  6838  xpf1o  6844  sbthlemi8  6963  sbthlemi9  6964  supelti  7001  supisoti  7009  djulclb  7054  nnnninfeq2  7127  cardcl  7180  isnumi  7181  cardval3ex  7184  exmidonfinlem  7192  en2eleq  7194  acfun  7206  exmidaclem  7207  dftap2  7250  exmidapne  7259  ccfunen  7263  indpi  7341  dfplpq2  7353  ltbtwnnq  7415  enq0tr  7433  nqnq0pi  7437  elnp1st2nd  7475  prcunqu  7484  prnmaxl  7487  prloc  7490  genpcuu  7519  addnqprllem  7526  addlocprlemeq  7532  addlocprlemgt  7533  addlocpr  7535  nqprxx  7545  gtnqex  7549  appdivnq  7562  prmuloclemcalc  7564  prmuloc  7565  mullocprlem  7569  ltprordil  7588  ltnqpri  7593  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemdisj  7605  ltexprlemloc  7606  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  ltexpri  7612  recexprlemell  7621  recexprlemelu  7622  recexprlemloc  7630  recexprlempr  7631  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  aptipr  7640  cauappcvgprlemlol  7646  cauappcvgprlemupu  7648  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdrl  7656  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemlol  7669  caucvgprlemupu  7671  caucvgprlemladdfu  7676  caucvgprlem1  7678  caucvgprlem2  7679  caucvgprprlemnjltk  7690  caucvgprprlemnbj  7692  caucvgprprlemlol  7697  caucvgprprlemupu  7699  caucvgprprlemexbt  7705  caucvgprprlem1  7708  caucvgprprlem2  7709  suplocexprlemrl  7716  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemub  7722  suplocexprlemlub  7723  ltsrprg  7746  gt0srpr  7747  recexgt0sr  7772  addgt0sr  7774  mulgt0sr  7777  map2psrprg  7804  suplocsrlemb  7805  suplocsrlem  7807  nnindnn  7892  axcaucvglemcau  7897  axpre-suploclemres  7900  apreap  8544  apreim  8560  mulge0  8576  apti  8579  mulap0bbd  8617  lble  8904  nnind  8935  recnz  9346  uzind  9364  eluzadd  9556  eluzsub  9557  ixxss1  9904  ixxss2  9905  ixxss12  9906  iccss2  9944  iccssioo2  9946  iccssico2  9947  elfzolt2  10156  ioom  10261  elicore  10267  flqltp1  10279  addmodlteq  10398  expcl2lemap  10532  expap0i  10552  hashennnuni  10759  crre  10866  caucvgre  10990  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemoverl  11030  sqrtge0  11042  fimaxre2  11235  climi  11295  reccn2ap  11321  climge0  11333  nnf1o  11384  sumpr  11421  fsump1i  11441  fsum00  11470  fsumparts  11478  mertenslemi1  11543  addsin  11750  subsin  11751  addcos  11754  subcos  11755  sinbnd2  11762  cosbnd2  11763  dvdsaddre2b  11848  evenelz  11872  4dvdseven  11922  infssuzcldc  11952  gcd0id  11980  gcd1  11988  bezoutlemstep  11998  dvdsgcdb  12014  mulgcd  12017  gcdzeq  12023  dvdsmulgcd  12026  sqgcd  12030  dvdssqlem  12031  bezoutr  12033  uzwodc  12038  lcmval  12063  lcmcllem  12067  lcmgcdlem  12077  lcmdvds  12079  lcmgcdeq  12083  lcmdvdsb  12084  mulgcddvds  12094  rpmulgcd2  12095  qredeu  12097  rpdvds  12099  divgcdcoprm0  12101  isprm3  12118  divgcdodd  12143  coprm  12144  rpexp  12153  sqrt2irr  12162  qdencl  12189  qeqnumdivden  12194  divnumden  12196  divdenle  12197  densq  12204  phimullem  12225  eulerthlem1  12227  eulerthlemrprm  12229  eulerthlemth  12232  prmdiveq  12236  prmdivdiv  12237  hashgcdeq  12239  phisum  12240  odzid  12244  reumodprminv  12253  oddn2prm  12261  pythagtriplem4  12268  pythagtriplem11  12274  pythagtriplem13  12276  pythagtriplem19  12282  pclemub  12287  pcprendvds2  12291  pcpre1  12292  pcpremul  12293  pceulem  12294  pczdvds  12313  pc2dvds  12329  pcaddlem  12338  pcmpt  12341  pcmpt2  12342  pcmptdvds  12343  pcprod  12344  pockthlem  12354  pockthg  12355  prmunb  12360  1arithlem4  12364  4sqlem7  12382  4sqlem8  12383  4sqlem9  12384  4sqlem10  12385  ennnfonelemom  12409  ennnfonelemex  12415  ennnfonelemf1  12419  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  fnpr2ob  12759  mgmlrid  12798  mndrid  12837  grpinvcnv  12938  dfgrp3mlem  12968  eqglact  13084  srgdilem  13152  srgdir  13158  srgridm  13163  ringdilem  13195  ringdir  13202  ringridm  13207  unitmulcl  13282  unitnegcl  13299  lringuplu  13337  subrgring  13345  subrg1cl  13350  inopn  13506  restbasg  13671  ssrest  13685  cntop2  13705  icnpimaex  13714  cnima  13723  lmfss  13747  lmtopcnp  13753  txhmeo  13822  txswaphmeo  13824  psmet0  13830  psmettri2  13831  blhalf  13911  bdxmet  14004  xmetxpbl  14011  ioo2bl  14046  tgioo  14049  cncfi  14068  rescncf  14071  cdivcncfap  14090  cnopnap  14097  dedekindeulemeu  14103  dedekindicclemeu  14112  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthinclemdisj  14121  ivthdec  14125  limcimo  14137  cnplimcim  14139  cnplimclemr  14141  cnlimci  14145  limccnpcntop  14147  limccnp2lem  14148  limccnp2cntop  14149  limccoap  14150  reldvg  14151  dvbsssg  14158  dvfgg  14160  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180  sin0pilem1  14205  sin0pilem2  14206  tanrpcl  14261  tangtx  14262  cos0pilt1  14276  logbgcd1irraplemexp  14389  lgsne0  14442  2sqlem8a  14472  2sqlem8  14473  bj-charfunbi  14566  bj-inf2vnlem1  14725  pwf1oexmid  14752  subctctexmid  14753  iooref1o  14785  taupi  14823  alsi2d  14832  alsc2d  14834