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  3223  unssbd  3397  opth  4353  potr  4429  frind  4473  brrelex2  4791  funinsn  5405  feu  5549  fcnvres  5550  fun11iun  5635  funopsn  5860  elmpocl2  6251  uchoice  6331  oprssdmm  6365  fczsupp0  6459  tfrlem1  6539  tfrlemisucfn  6555  tfrlemisucaccv  6556  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrlemi14d  6564  swoer  6795  elmapssres  6907  mapsspm  6916  pmsspw  6917  mapss  6926  dom0  7091  xpf1o  7097  sbthlemi8  7234  sbthlemi9  7235  fsuppimpd  7246  supelti  7293  supisoti  7301  djulclb  7346  nninfninc  7414  nnnninfeq2  7420  cardcl  7477  isnumi  7478  cardval3ex  7481  exmidonfinlem  7496  en2eleq  7498  finacn  7511  acfun  7514  exmidaclem  7515  pw1if  7535  papirr  7560  dftap2  7565  exmidapne  7574  ccfunen  7578  acnccim  7586  indpi  7657  dfplpq2  7669  ltbtwnnq  7731  enq0tr  7749  nqnq0pi  7753  elnp1st2nd  7791  prcunqu  7800  prnmaxl  7803  prloc  7806  genpcuu  7835  addnqprllem  7842  addlocprlemeq  7848  addlocprlemgt  7849  addlocpr  7851  nqprxx  7861  gtnqex  7865  appdivnq  7878  prmuloclemcalc  7880  prmuloc  7881  mullocprlem  7885  ltprordil  7904  ltnqpri  7909  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  ltexpri  7928  recexprlemell  7937  recexprlemelu  7938  recexprlemloc  7946  recexprlempr  7947  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  aptipr  7956  cauappcvgprlemlol  7962  cauappcvgprlemupu  7964  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdrl  7972  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemlol  7985  caucvgprlemupu  7987  caucvgprlemladdfu  7992  caucvgprlem1  7994  caucvgprlem2  7995  caucvgprprlemnjltk  8006  caucvgprprlemnbj  8008  caucvgprprlemlol  8013  caucvgprprlemupu  8015  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  suplocexprlemrl  8032  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemub  8038  suplocexprlemlub  8039  ltsrprg  8062  gt0srpr  8063  recexgt0sr  8088  addgt0sr  8090  mulgt0sr  8093  map2psrprg  8120  suplocsrlemb  8121  suplocsrlem  8123  nnindnn  8208  axcaucvglemcau  8213  axpre-suploclemres  8216  apreap  8861  apreim  8877  mulge0  8893  apti  8896  mulap0bbd  8934  lble  9221  nnind  9253  recnz  9671  uzind  9689  eluzadd  9883  eluzsub  9884  ixxss1  10237  ixxss2  10238  ixxss12  10239  iccss2  10277  iccssioo2  10279  iccssico2  10280  elfzolt2  10491  infssuzcldc  10595  ioom  10620  elicore  10626  flqltp1  10639  addmodlteq  10760  expcl2lemap  10913  expap0i  10933  hashennnuni  11142  hashdmprop2dom  11216  wrdexb  11236  swrdsbslen  11358  swrdspsleq  11359  crre  11542  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemoverl  11706  sqrtge0  11718  fimaxre2  11912  climi  11972  reccn2ap  11998  climge0  12010  nnf1o  12062  sumpr  12099  fsump1i  12119  fsum00  12148  fsumparts  12156  mertenslemi1  12221  addsin  12428  subsin  12429  addcos  12432  subcos  12433  sinbnd2  12440  cosbnd2  12441  sinltxirr  12447  dvdsaddre2b  12527  evenelz  12553  4dvdseven  12603  gcd0id  12675  gcd1  12683  bezoutlemstep  12693  dvdsgcdb  12709  mulgcd  12712  gcdzeq  12718  dvdsmulgcd  12721  sqgcd  12725  dvdssqlem  12726  bezoutr  12728  uzwodc  12733  nninfctlemfo  12736  lcmval  12760  lcmcllem  12764  lcmgcdlem  12774  lcmdvds  12776  lcmgcdeq  12780  lcmdvdsb  12781  mulgcddvds  12791  rpmulgcd2  12792  qredeu  12794  rpdvds  12796  divgcdcoprm0  12798  isprm3  12815  divgcdodd  12840  coprm  12841  rpexp  12850  sqrt2irr  12859  qdencl  12886  qeqnumdivden  12891  divnumden  12893  divdenle  12894  densq  12901  phimullem  12922  eulerthlem1  12924  eulerthlemrprm  12926  eulerthlemth  12929  prmdiveq  12933  prmdivdiv  12934  hashgcdeq  12937  phisum  12938  odzid  12942  reumodprminv  12951  oddn2prm  12959  pythagtriplem4  12966  pythagtriplem11  12972  pythagtriplem13  12974  pythagtriplem19  12980  pclemub  12985  pcprendvds2  12989  pcpre1  12990  pcpremul  12991  pceulem  12992  pczdvds  13012  pc2dvds  13028  pcaddlem  13037  pcmpt  13041  pcmpt2  13042  pcmptdvds  13043  pcprod  13044  pockthlem  13054  pockthg  13055  prmunb  13060  1arithlem4  13064  4sqlem7  13082  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqlemffi  13094  4sqlem15  13103  4sqlem16  13104  4sqlem17  13105  4sqlem18  13106  ballotfilem2  13142  ennnfonelemom  13159  ennnfonelemex  13165  ennnfonelemf1  13169  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  fnpr2ob  13553  mgmlrid  13592  gsumfzval  13604  gsumval2  13610  mndrid  13649  prdsmndd  13661  grpinvcnv  13781  dfgrp3mlem  13811  prdsgrpd  13822  prdsinvgd  13823  eqglact  13942  ghmgrp2  13963  ghmlin  13965  ghmnsgpreima  13986  kerf1ghm  13991  gsumsplit0  14063  srgdilem  14113  srgdir  14119  srgridm  14124  ringdilem  14156  ringdir  14163  ringridm  14168  unitmulcl  14258  unitnegcl  14275  rhmmhm  14304  elrhmunit  14322  lringuplu  14341  subrgring  14369  subrg1cl  14374  qusrhm  14676  znunit  14807  znrrg  14808  psrbagfsupp  14819  psrbaglecl  14824  psrbagcon  14826  psrbagconcl  14827  psrelbas  14830  mplsubgfilemcl  14854  mplsubgfileminv  14855  inopn  14868  restbasg  15033  ssrest  15047  cntop2  15067  icnpimaex  15076  cnima  15085  lmfss  15109  lmtopcnp  15115  txhmeo  15184  txswaphmeo  15186  psmet0  15192  psmettri2  15193  blhalf  15273  bdxmet  15366  xmetxpbl  15373  ioo2bl  15416  tgioo  15419  cncfi  15443  rescncf  15446  cdivcncfap  15469  cnopnap  15476  divcncfap  15479  dedekindeulemeu  15487  dedekindicclemeu  15496  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthinclemdisj  15505  ivthdec  15509  ivthreinc  15510  limcimo  15530  cnplimcim  15532  cnplimclemr  15534  cnlimci  15538  limccnpcntop  15540  limccnp2lem  15541  limccnp2cntop  15542  limccoap  15543  reldvg  15544  dvbsssg  15551  dvfgg  15553  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  plyco  15624  plycj  15626  plyrecj  15628  sin0pilem1  15646  sin0pilem2  15647  tanrpcl  15702  tangtx  15703  cos0pilt1  15717  logbgcd1irraplemexp  15833  mpodvdsmulf1o  15858  perfect  15869  lgsne0  15911  lgseisen  15947  lgsquad2lem2  15955  2sqlem8a  15995  2sqlem8  15996  structgrssiedg  16038  uhgrm  16073  umgredgne  16145  usgruspgrben  16181  usgredgppren  16192  umgr2edg  16202  vtxdumgrfival  16293  wlkpropg  16319  wlkv  16321  wlkvtxeledgg  16339  g0wlk0  16365  trlsv  16379  clwwlknlen  16406  eupthv  16441  eupthf1o  16445  eupth2lem3lem4fi  16468  eulerpathprum  16475  bj-charfunbi  16581  bj-inf2vnlem1  16740  pwf1oexmid  16773  subctctexmid  16774  iooref1o  16818  taupi  16859  alsi2d  16879  alsc2d  16881