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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  biimpr  130  simprbi  275  simplbda  384  simplrd  534  simprld  536  simprrd  538  simp2  1029  simp3  1030  sbh  1829  eldifbd  3232  unssbd  3407  opth  4377  potr  4453  frind  4497  brrelex2  4816  funinsn  5430  feu  5574  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl2  6286  uchoice  6371  oprssdmm  6405  fczsupp0  6499  tfrlem1  6579  tfrlemisucfn  6595  tfrlemisucaccv  6596  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemi14d  6604  swoer  6835  elmapssres  6954  mapsspm  6963  pmsspw  6964  mapss  6973  dom0  7138  xpf1o  7144  sbthlemi8  7281  sbthlemi9  7282  fsuppimpd  7293  supelti  7342  supisoti  7350  djulclb  7395  nninfninc  7463  nnnninfeq2  7469  cardcl  7526  isnumi  7527  cardval3ex  7530  exmidonfinlem  7545  en2eleq  7547  finacn  7560  acfun  7563  exmidaclem  7564  pw1if  7584  papirr  7611  dftap2  7617  exmidapne  7626  ccfunen  7630  acnccim  7638  indpi  7709  dfplpq2  7721  ltbtwnnq  7783  enq0tr  7801  nqnq0pi  7805  elnp1st2nd  7843  prcunqu  7852  prnmaxl  7855  prloc  7858  genpcuu  7887  addnqprllem  7894  addlocprlemeq  7900  addlocprlemgt  7901  addlocpr  7903  nqprxx  7913  gtnqex  7917  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  aptipr  8008  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdrl  8024  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprlemladdfu  8044  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnjltk  8058  caucvgprprlemnbj  8060  caucvgprprlemlol  8065  caucvgprprlemupu  8067  caucvgprprlemexbt  8073  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemub  8090  suplocexprlemlub  8091  ltsrprg  8114  gt0srpr  8115  recexgt0sr  8140  addgt0sr  8142  mulgt0sr  8145  map2psrprg  8172  suplocsrlemb  8173  suplocsrlem  8175  nnindnn  8260  axcaucvglemcau  8265  axpre-suploclemres  8268  apreap  8915  apreim  8931  mulge0  8947  apti  8950  mulap0bbd  8988  lble  9277  nnind  9320  recnz  9739  uzind  9757  eluzadd  9951  eluzsub  9952  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccss2  10346  iccssioo2  10348  iccssico2  10349  elfzolt2  10564  infssuzcldc  10668  ioom  10695  elicore  10701  flqltp1  10714  addmodlteq  10835  expcl2lemap  10988  expap0i  11008  hashennnuni  11218  hashf1lem2  11286  hashdmprop2dom  11296  wrdexb  11316  swrdsbslen  11438  swrdspsleq  11439  crre  11622  sq01  11660  caucvgre  11747  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemoverl  11787  sqrtge0  11799  fimaxre2  11993  climi  12053  reccn2ap  12079  climge0  12091  nnf1o  12143  sumpr  12180  fsump1i  12200  fsum00  12229  fsumparts  12237  mertenslemi1  12302  addsin  12509  subsin  12510  addcos  12513  subcos  12514  sinbnd2  12521  cosbnd2  12522  sinltxirr  12528  dvdsaddre2b  12608  evenelz  12634  4dvdseven  12684  gcd0id  12756  gcd1  12764  bezoutlemstep  12774  dvdsgcdb  12790  mulgcd  12793  gcdzeq  12799  dvdsmulgcd  12802  sqgcd  12806  dvdssqlem  12807  bezoutr  12809  uzwodc  12814  nninfctlemfo  12817  lcmval  12841  lcmcllem  12845  lcmgcdlem  12855  lcmdvds  12857  lcmgcdeq  12861  lcmdvdsb  12862  mulgcddvds  12872  rpmulgcd2  12873  qredeu  12875  rpdvds  12877  divgcdcoprm0  12879  isprm3  12896  divgcdodd  12921  coprm  12922  rpexp  12931  sqrt2irr  12940  qdencl  12967  qeqnumdivden  12972  divnumden  12974  divdenle  12975  densq  12982  phimullem  13003  eulerthlem1  13005  eulerthlemrprm  13007  eulerthlemth  13010  prmdiveq  13014  prmdivdiv  13015  hashgcdeq  13018  phisum  13019  odzid  13023  reumodprminv  13032  oddn2prm  13040  pythagtriplem4  13047  pythagtriplem11  13053  pythagtriplem13  13055  pythagtriplem19  13061  pclemub  13066  pcprendvds2  13070  pcpre1  13071  pcpremul  13072  pceulem  13073  pczdvds  13093  pc2dvds  13109  pcaddlem  13118  pcmpt  13122  pcmpt2  13123  pcmptdvds  13124  pcprod  13125  pockthlem  13135  pockthg  13136  prmunb  13141  1arithlem4  13145  4sqlem7  13163  4sqlem8  13164  4sqlem9  13165  4sqlem10  13166  4sqlemffi  13175  4sqlem15  13184  4sqlem16  13185  4sqlem17  13186  4sqlem18  13187  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsf1o  13257  ballotfilemscr  13262  ballotfilemrv  13263  ballotfilemfrci  13271  ballotfilemfrceq  13272  ballotfilemrinv0  13276  ennnfonelemom  13299  ennnfonelemex  13305  ennnfonelemf1  13309  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  fnpr2ob  13661  mgmlrid  13699  gzsumfzval  13711  gzsumval2  13714  mndrid  13749  grpinvcnv  13873  dfgrp3mlem  13903  eqglact  14028  ghmgrp2  14049  ghmlin  14051  ghmnsgpreima  14072  kerf1ghm  14077  gzsumsplit0  14148  prdsmndd  14194  prdsgrpd  14197  prdsinvgd  14198  srgdilem  14273  srgdir  14279  srgridm  14284  ringdilem  14316  ringdir  14324  ringridm  14329  unitmulcl  14420  unitnegcl  14437  rhmmhm  14466  elrhmunit  14484  lringuplu  14503  subrgring  14532  subrg1cl  14537  qusrhm  14865  znunit  14994  znrrg  14995  assaassr  15005  assaring  15007  psrbagfsupp  15055  psrbaglecl  15060  psrbagcon  15062  psrbagconcl  15063  psrelbas  15066  mplsubgfilemcl  15090  mplsubgfileminv  15091  inopn  15104  restbasg  15269  ssrest  15283  cntop2  15303  icnpimaex  15312  cnima  15321  lmfss  15345  lmtopcnp  15351  txhmeo  15420  txswaphmeo  15422  psmet0  15428  psmettri2  15429  blhalf  15509  bdxmet  15602  xmetxpbl  15609  ioo2bl  15652  tgioo  15655  cncfi  15679  rescncf  15682  cdivcncfap  15705  cnopnap  15712  divcncfap  15715  dedekindeulemeu  15723  dedekindicclemeu  15732  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthinclemdisj  15741  ivthdec  15745  ivthreinc  15746  limcimo  15766  cnplimcim  15768  cnplimclemr  15770  cnlimci  15774  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  limccoap  15779  reldvg  15780  dvbsssg  15787  dvfgg  15789  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcjbr  15809  dvrecap  15814  plyco  15860  plycj  15862  plyrecj  15864  sin0pilem1  15882  sin0pilem2  15883  tanrpcl  15938  tangtx  15939  cos0pilt1  15953  logbgcd1irraplemexp  16070  mpodvdsmulf1o  16104  perfect  16115  lgsne0  16157  lgseisen  16193  lgsquad2lem2  16201  2sqlem8a  16241  2sqlem8  16242  structgrssiedg  16284  uhgrm  16319  umgredgne  16391  usgruspgrben  16427  usgredgppren  16438  umgr2edg  16448  vtxdumgrfival  16539  wlkpropg  16565  wlkv  16567  wlkvtxeledgg  16585  g0wlk0  16611  trlsv  16625  clwwlknlen  16652  eupthv  16687  eupthf1o  16691  eupth2lem3lem4fi  16714  eulerpathprum  16721  bj-charfunbi  16837  bj-inf2vnlem1  16996  pwf1oexmid  17029  subctctexmid  17030  iooref1o  17083  taupi  17123  als2d  17134  rals2d  17136  alseu2d  17170  ralseu2d  17172