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  1025  simp3  1026  sbh  1825  eldifbd  3226  unssbd  3401  opth  4358  potr  4434  frind  4478  brrelex2  4796  funinsn  5410  feu  5554  fcnvres  5555  fun11iun  5640  funopsn  5865  elmpocl2  6259  uchoice  6344  oprssdmm  6378  fczsupp0  6472  tfrlem1  6552  tfrlemisucfn  6568  tfrlemisucaccv  6569  tfrlemibxssdm  6571  tfrlemibfn  6572  tfrlemi14d  6577  swoer  6808  elmapssres  6920  mapsspm  6929  pmsspw  6930  mapss  6939  dom0  7104  xpf1o  7110  sbthlemi8  7247  sbthlemi9  7248  fsuppimpd  7259  supelti  7306  supisoti  7314  djulclb  7359  nninfninc  7427  nnnninfeq2  7433  cardcl  7490  isnumi  7491  cardval3ex  7494  exmidonfinlem  7509  en2eleq  7511  finacn  7524  acfun  7527  exmidaclem  7528  pw1if  7548  papirr  7575  dftap2  7581  exmidapne  7590  ccfunen  7594  acnccim  7602  indpi  7673  dfplpq2  7685  ltbtwnnq  7747  enq0tr  7765  nqnq0pi  7769  elnp1st2nd  7807  prcunqu  7816  prnmaxl  7819  prloc  7822  genpcuu  7851  addnqprllem  7858  addlocprlemeq  7864  addlocprlemgt  7865  addlocpr  7867  nqprxx  7877  gtnqex  7881  appdivnq  7894  prmuloclemcalc  7896  prmuloc  7897  mullocprlem  7901  ltprordil  7920  ltnqpri  7925  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  ltexpri  7944  recexprlemell  7953  recexprlemelu  7954  recexprlemloc  7962  recexprlempr  7963  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  aptipr  7972  cauappcvgprlemlol  7978  cauappcvgprlemupu  7980  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdrl  7988  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemlol  8001  caucvgprlemupu  8003  caucvgprlemladdfu  8008  caucvgprlem1  8010  caucvgprlem2  8011  caucvgprprlemnjltk  8022  caucvgprprlemnbj  8024  caucvgprprlemlol  8029  caucvgprprlemupu  8031  caucvgprprlemexbt  8037  caucvgprprlem1  8040  caucvgprprlem2  8041  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemub  8054  suplocexprlemlub  8055  ltsrprg  8078  gt0srpr  8079  recexgt0sr  8104  addgt0sr  8106  mulgt0sr  8109  map2psrprg  8136  suplocsrlemb  8137  suplocsrlem  8139  nnindnn  8224  axcaucvglemcau  8229  axpre-suploclemres  8232  apreap  8878  apreim  8894  mulge0  8910  apti  8913  mulap0bbd  8951  lble  9238  nnind  9270  recnz  9689  uzind  9707  eluzadd  9901  eluzsub  9902  ixxss1  10256  ixxss2  10257  ixxss12  10258  iccss2  10296  iccssioo2  10298  iccssico2  10299  elfzolt2  10513  infssuzcldc  10617  ioom  10644  elicore  10650  flqltp1  10663  addmodlteq  10784  expcl2lemap  10937  expap0i  10957  hashennnuni  11167  hashdmprop2dom  11241  wrdexb  11261  swrdsbslen  11383  swrdspsleq  11384  crre  11567  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemoverl  11731  sqrtge0  11743  fimaxre2  11937  climi  11997  reccn2ap  12023  climge0  12035  nnf1o  12087  sumpr  12124  fsump1i  12144  fsum00  12173  fsumparts  12181  mertenslemi1  12246  addsin  12453  subsin  12454  addcos  12457  subcos  12458  sinbnd2  12465  cosbnd2  12466  sinltxirr  12472  dvdsaddre2b  12552  evenelz  12578  4dvdseven  12628  gcd0id  12700  gcd1  12708  bezoutlemstep  12718  dvdsgcdb  12734  mulgcd  12737  gcdzeq  12743  dvdsmulgcd  12746  sqgcd  12750  dvdssqlem  12751  bezoutr  12753  uzwodc  12758  nninfctlemfo  12761  lcmval  12785  lcmcllem  12789  lcmgcdlem  12799  lcmdvds  12801  lcmgcdeq  12805  lcmdvdsb  12806  mulgcddvds  12816  rpmulgcd2  12817  qredeu  12819  rpdvds  12821  divgcdcoprm0  12823  isprm3  12840  divgcdodd  12865  coprm  12866  rpexp  12875  sqrt2irr  12884  qdencl  12911  qeqnumdivden  12916  divnumden  12918  divdenle  12919  densq  12926  phimullem  12947  eulerthlem1  12949  eulerthlemrprm  12951  eulerthlemth  12954  prmdiveq  12958  prmdivdiv  12959  hashgcdeq  12962  phisum  12963  odzid  12967  reumodprminv  12976  oddn2prm  12984  pythagtriplem4  12991  pythagtriplem11  12997  pythagtriplem13  12999  pythagtriplem19  13005  pclemub  13010  pcprendvds2  13014  pcpre1  13015  pcpremul  13016  pceulem  13017  pczdvds  13037  pc2dvds  13053  pcaddlem  13062  pcmpt  13066  pcmpt2  13067  pcmptdvds  13068  pcprod  13069  pockthlem  13079  pockthg  13080  prmunb  13085  1arithlem4  13089  4sqlem7  13107  4sqlem8  13108  4sqlem9  13109  4sqlem10  13110  4sqlemffi  13119  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  4sqlem18  13131  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsf1o  13201  ballotfilemscr  13206  ballotfilemrv  13207  ballotfilemfrci  13215  ballotfilemfrceq  13216  ballotfilemrinv0  13220  ennnfonelemom  13243  ennnfonelemex  13249  ennnfonelemf1  13253  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  fnpr2ob  13604  mgmlrid  13642  gsumfzval  13654  gsumval2  13660  mndrid  13697  grpinvcnv  13823  dfgrp3mlem  13853  eqglact  13978  ghmgrp2  13999  ghmlin  14001  ghmnsgpreima  14022  kerf1ghm  14027  gsumsplit0  14099  prdsmndd  14136  prdsgrpd  14139  prdsinvgd  14140  srgdilem  14212  srgdir  14218  srgridm  14223  ringdilem  14255  ringdir  14262  ringridm  14267  unitmulcl  14358  unitnegcl  14375  rhmmhm  14404  elrhmunit  14422  lringuplu  14441  subrgring  14470  subrg1cl  14475  qusrhm  14802  znunit  14933  znrrg  14934  psrbagfsupp  14945  psrbaglecl  14950  psrbagcon  14952  psrbagconcl  14953  psrelbas  14956  mplsubgfilemcl  14980  mplsubgfileminv  14981  inopn  14994  restbasg  15159  ssrest  15173  cntop2  15193  icnpimaex  15202  cnima  15211  lmfss  15235  lmtopcnp  15241  txhmeo  15310  txswaphmeo  15312  psmet0  15318  psmettri2  15319  blhalf  15399  bdxmet  15492  xmetxpbl  15499  ioo2bl  15542  tgioo  15545  cncfi  15569  rescncf  15572  cdivcncfap  15595  cnopnap  15602  divcncfap  15605  dedekindeulemeu  15613  dedekindicclemeu  15622  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthinclemdisj  15631  ivthdec  15635  ivthreinc  15636  limcimo  15656  cnplimcim  15658  cnplimclemr  15660  cnlimci  15664  limccnpcntop  15666  limccnp2lem  15667  limccnp2cntop  15668  limccoap  15669  reldvg  15670  dvbsssg  15677  dvfgg  15679  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvrecap  15704  plyco  15750  plycj  15752  plyrecj  15754  sin0pilem1  15772  sin0pilem2  15773  tanrpcl  15828  tangtx  15829  cos0pilt1  15843  logbgcd1irraplemexp  15959  mpodvdsmulf1o  15984  perfect  15995  lgsne0  16037  lgseisen  16073  lgsquad2lem2  16081  2sqlem8a  16121  2sqlem8  16122  structgrssiedg  16164  uhgrm  16199  umgredgne  16271  usgruspgrben  16307  usgredgppren  16318  umgr2edg  16328  vtxdumgrfival  16419  wlkpropg  16445  wlkv  16447  wlkvtxeledgg  16465  g0wlk0  16491  trlsv  16505  clwwlknlen  16532  eupthv  16567  eupthf1o  16571  eupth2lem3lem4fi  16594  eulerpathprum  16601  bj-charfunbi  16707  bj-inf2vnlem1  16866  pwf1oexmid  16899  subctctexmid  16900  iooref1o  16944  taupi  16985  alsi2d  16994  alsc2d  16996