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  simplrd  530  simprld  532  simprrd  534  simp2  1024  simp3  1025  sbh  1824  eldifbd  3212  unssbd  3385  opth  4329  potr  4405  frind  4449  brrelex2  4767  funinsn  5379  feu  5519  fcnvres  5520  fun11iun  5604  funopsn  5829  elmpocl2  6218  uchoice  6299  oprssdmm  6333  tfrlem1  6473  tfrlemisucfn  6489  tfrlemisucaccv  6490  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemi14d  6498  swoer  6729  elmapssres  6841  mapsspm  6850  pmsspw  6851  mapss  6859  dom0  7023  xpf1o  7029  sbthlemi8  7162  sbthlemi9  7163  supelti  7200  supisoti  7208  djulclb  7253  nninfninc  7321  nnnninfeq2  7327  cardcl  7384  isnumi  7385  cardval3ex  7388  exmidonfinlem  7403  en2eleq  7405  finacn  7418  acfun  7421  exmidaclem  7422  pw1if  7442  dftap2  7469  exmidapne  7478  ccfunen  7482  acnccim  7490  indpi  7561  dfplpq2  7573  ltbtwnnq  7635  enq0tr  7653  nqnq0pi  7657  elnp1st2nd  7695  prcunqu  7704  prnmaxl  7707  prloc  7710  genpcuu  7739  addnqprllem  7746  addlocprlemeq  7752  addlocprlemgt  7753  addlocpr  7755  nqprxx  7765  gtnqex  7769  appdivnq  7782  prmuloclemcalc  7784  prmuloc  7785  mullocprlem  7789  ltprordil  7808  ltnqpri  7813  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemfl  7828  ltexprlemrl  7829  ltexprlemfu  7830  ltexprlemru  7831  ltexpri  7832  recexprlemell  7841  recexprlemelu  7842  recexprlemloc  7850  recexprlempr  7851  recexprlem1ssl  7852  recexprlem1ssu  7853  recexprlemss1l  7854  aptipr  7860  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlemladdrl  7876  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprlemladdfu  7896  caucvgprlem1  7898  caucvgprlem2  7899  caucvgprprlemnjltk  7910  caucvgprprlemnbj  7912  caucvgprprlemlol  7917  caucvgprprlemupu  7919  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  suplocexprlemrl  7936  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemub  7942  suplocexprlemlub  7943  ltsrprg  7966  gt0srpr  7967  recexgt0sr  7992  addgt0sr  7994  mulgt0sr  7997  map2psrprg  8024  suplocsrlemb  8025  suplocsrlem  8027  nnindnn  8112  axcaucvglemcau  8117  axpre-suploclemres  8120  apreap  8766  apreim  8782  mulge0  8798  apti  8801  mulap0bbd  8839  lble  9126  nnind  9158  recnz  9572  uzind  9590  eluzadd  9784  eluzsub  9785  ixxss1  10138  ixxss2  10139  ixxss12  10140  iccss2  10178  iccssioo2  10180  iccssico2  10181  elfzolt2  10391  infssuzcldc  10494  ioom  10519  elicore  10525  flqltp1  10538  addmodlteq  10659  expcl2lemap  10812  expap0i  10832  hashennnuni  11040  hashdmprop2dom  11107  wrdexb  11124  swrdsbslen  11246  swrdspsleq  11247  crre  11417  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemoverl  11581  sqrtge0  11593  fimaxre2  11787  climi  11847  reccn2ap  11873  climge0  11885  nnf1o  11936  sumpr  11973  fsump1i  11993  fsum00  12022  fsumparts  12030  mertenslemi1  12095  addsin  12302  subsin  12303  addcos  12306  subcos  12307  sinbnd2  12314  cosbnd2  12315  sinltxirr  12321  dvdsaddre2b  12401  evenelz  12427  4dvdseven  12477  gcd0id  12549  gcd1  12557  bezoutlemstep  12567  dvdsgcdb  12583  mulgcd  12586  gcdzeq  12592  dvdsmulgcd  12595  sqgcd  12599  dvdssqlem  12600  bezoutr  12602  uzwodc  12607  nninfctlemfo  12610  lcmval  12634  lcmcllem  12638  lcmgcdlem  12648  lcmdvds  12650  lcmgcdeq  12654  lcmdvdsb  12655  mulgcddvds  12665  rpmulgcd2  12666  qredeu  12668  rpdvds  12670  divgcdcoprm0  12672  isprm3  12689  divgcdodd  12714  coprm  12715  rpexp  12724  sqrt2irr  12733  qdencl  12760  qeqnumdivden  12765  divnumden  12767  divdenle  12768  densq  12775  phimullem  12796  eulerthlem1  12798  eulerthlemrprm  12800  eulerthlemth  12803  prmdiveq  12807  prmdivdiv  12808  hashgcdeq  12811  phisum  12812  odzid  12816  reumodprminv  12825  oddn2prm  12833  pythagtriplem4  12840  pythagtriplem11  12846  pythagtriplem13  12848  pythagtriplem19  12854  pclemub  12859  pcprendvds2  12863  pcpre1  12864  pcpremul  12865  pceulem  12866  pczdvds  12886  pc2dvds  12902  pcaddlem  12911  pcmpt  12915  pcmpt2  12916  pcmptdvds  12917  pcprod  12918  pockthlem  12928  pockthg  12929  prmunb  12934  1arithlem4  12938  4sqlem7  12956  4sqlem8  12957  4sqlem9  12958  4sqlem10  12959  4sqlemffi  12968  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  4sqlem18  12980  ennnfonelemom  13028  ennnfonelemex  13034  ennnfonelemf1  13038  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  fnpr2ob  13422  mgmlrid  13461  gsumfzval  13473  gsumval2  13479  mndrid  13518  prdsmndd  13530  grpinvcnv  13650  dfgrp3mlem  13680  prdsgrpd  13691  prdsinvgd  13692  eqglact  13811  ghmgrp2  13832  ghmlin  13834  ghmnsgpreima  13855  kerf1ghm  13860  srgdilem  13981  srgdir  13987  srgridm  13992  ringdilem  14024  ringdir  14031  ringridm  14036  unitmulcl  14126  unitnegcl  14143  rhmmhm  14172  elrhmunit  14190  lringuplu  14209  subrgring  14237  subrg1cl  14242  qusrhm  14541  znunit  14672  znrrg  14673  psrelbas  14688  mplsubgfilemcl  14712  mplsubgfileminv  14713  inopn  14726  restbasg  14891  ssrest  14905  cntop2  14925  icnpimaex  14934  cnima  14943  lmfss  14967  lmtopcnp  14973  txhmeo  15042  txswaphmeo  15044  psmet0  15050  psmettri2  15051  blhalf  15131  bdxmet  15224  xmetxpbl  15231  ioo2bl  15274  tgioo  15277  cncfi  15301  rescncf  15304  cdivcncfap  15327  cnopnap  15334  divcncfap  15337  dedekindeulemeu  15345  dedekindicclemeu  15354  ivthinclemum  15358  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthinclemdisj  15363  ivthdec  15367  ivthreinc  15368  limcimo  15388  cnplimcim  15390  cnplimclemr  15392  cnlimci  15396  limccnpcntop  15398  limccnp2lem  15399  limccnp2cntop  15400  limccoap  15401  reldvg  15402  dvbsssg  15409  dvfgg  15411  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  plyco  15482  plycj  15484  plyrecj  15486  sin0pilem1  15504  sin0pilem2  15505  tanrpcl  15560  tangtx  15561  cos0pilt1  15575  logbgcd1irraplemexp  15691  mpodvdsmulf1o  15713  perfect  15724  lgsne0  15766  lgseisen  15802  lgsquad2lem2  15810  2sqlem8a  15850  2sqlem8  15851  structgrssiedg  15893  uhgrm  15928  umgredgne  16000  usgruspgrben  16036  usgredgppren  16047  umgr2edg  16057  vtxdumgrfival  16148  wlkpropg  16174  wlkv  16176  wlkvtxeledgg  16194  g0wlk0  16220  trlsv  16234  clwwlknlen  16261  eupthv  16296  eupthf1o  16300  bj-charfunbi  16406  bj-inf2vnlem1  16565  pwf1oexmid  16600  subctctexmid  16601  iooref1o  16638  taupi  16677  alsi2d  16693  alsc2d  16695