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  5830  elmpocl2  6219  uchoice  6300  oprssdmm  6334  tfrlem1  6474  tfrlemisucfn  6490  tfrlemisucaccv  6491  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemi14d  6499  swoer  6730  elmapssres  6842  mapsspm  6851  pmsspw  6852  mapss  6860  dom0  7024  xpf1o  7030  sbthlemi8  7163  sbthlemi9  7164  supelti  7201  supisoti  7209  djulclb  7254  nninfninc  7322  nnnninfeq2  7328  cardcl  7385  isnumi  7386  cardval3ex  7389  exmidonfinlem  7404  en2eleq  7406  finacn  7419  acfun  7422  exmidaclem  7423  pw1if  7443  dftap2  7470  exmidapne  7479  ccfunen  7483  acnccim  7491  indpi  7562  dfplpq2  7574  ltbtwnnq  7636  enq0tr  7654  nqnq0pi  7658  elnp1st2nd  7696  prcunqu  7705  prnmaxl  7708  prloc  7711  genpcuu  7740  addnqprllem  7747  addlocprlemeq  7753  addlocprlemgt  7754  addlocpr  7756  nqprxx  7766  gtnqex  7770  appdivnq  7783  prmuloclemcalc  7785  prmuloc  7786  mullocprlem  7790  ltprordil  7809  ltnqpri  7814  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  ltexpri  7833  recexprlemell  7842  recexprlemelu  7843  recexprlemloc  7851  recexprlempr  7852  recexprlem1ssl  7853  recexprlem1ssu  7854  recexprlemss1l  7855  aptipr  7861  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlemladdrl  7877  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprlemladdfu  7897  caucvgprlem1  7899  caucvgprlem2  7900  caucvgprprlemnjltk  7911  caucvgprprlemnbj  7913  caucvgprprlemlol  7918  caucvgprprlemupu  7920  caucvgprprlemexbt  7926  caucvgprprlem1  7929  caucvgprprlem2  7930  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemub  7943  suplocexprlemlub  7944  ltsrprg  7967  gt0srpr  7968  recexgt0sr  7993  addgt0sr  7995  mulgt0sr  7998  map2psrprg  8025  suplocsrlemb  8026  suplocsrlem  8028  nnindnn  8113  axcaucvglemcau  8118  axpre-suploclemres  8121  apreap  8767  apreim  8783  mulge0  8799  apti  8802  mulap0bbd  8840  lble  9127  nnind  9159  recnz  9573  uzind  9591  eluzadd  9785  eluzsub  9786  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssioo2  10181  iccssico2  10182  elfzolt2  10392  infssuzcldc  10496  ioom  10521  elicore  10527  flqltp1  10540  addmodlteq  10661  expcl2lemap  10814  expap0i  10834  hashennnuni  11042  hashdmprop2dom  11109  wrdexb  11129  swrdsbslen  11251  swrdspsleq  11252  crre  11435  caucvgre  11559  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemoverl  11599  sqrtge0  11611  fimaxre2  11805  climi  11865  reccn2ap  11891  climge0  11903  nnf1o  11955  sumpr  11992  fsump1i  12012  fsum00  12041  fsumparts  12049  mertenslemi1  12114  addsin  12321  subsin  12322  addcos  12325  subcos  12326  sinbnd2  12333  cosbnd2  12334  sinltxirr  12340  dvdsaddre2b  12420  evenelz  12446  4dvdseven  12496  gcd0id  12568  gcd1  12576  bezoutlemstep  12586  dvdsgcdb  12602  mulgcd  12605  gcdzeq  12611  dvdsmulgcd  12614  sqgcd  12618  dvdssqlem  12619  bezoutr  12621  uzwodc  12626  nninfctlemfo  12629  lcmval  12653  lcmcllem  12657  lcmgcdlem  12667  lcmdvds  12669  lcmgcdeq  12673  lcmdvdsb  12674  mulgcddvds  12684  rpmulgcd2  12685  qredeu  12687  rpdvds  12689  divgcdcoprm0  12691  isprm3  12708  divgcdodd  12733  coprm  12734  rpexp  12743  sqrt2irr  12752  qdencl  12779  qeqnumdivden  12784  divnumden  12786  divdenle  12787  densq  12794  phimullem  12815  eulerthlem1  12817  eulerthlemrprm  12819  eulerthlemth  12822  prmdiveq  12826  prmdivdiv  12827  hashgcdeq  12830  phisum  12831  odzid  12835  reumodprminv  12844  oddn2prm  12852  pythagtriplem4  12859  pythagtriplem11  12865  pythagtriplem13  12867  pythagtriplem19  12873  pclemub  12878  pcprendvds2  12882  pcpre1  12883  pcpremul  12884  pceulem  12885  pczdvds  12905  pc2dvds  12921  pcaddlem  12930  pcmpt  12934  pcmpt2  12935  pcmptdvds  12936  pcprod  12937  pockthlem  12947  pockthg  12948  prmunb  12953  1arithlem4  12957  4sqlem7  12975  4sqlem8  12976  4sqlem9  12977  4sqlem10  12978  4sqlemffi  12987  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  4sqlem18  12999  ennnfonelemom  13047  ennnfonelemex  13053  ennnfonelemf1  13057  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  fnpr2ob  13441  mgmlrid  13480  gsumfzval  13492  gsumval2  13498  mndrid  13537  prdsmndd  13549  grpinvcnv  13669  dfgrp3mlem  13699  prdsgrpd  13710  prdsinvgd  13711  eqglact  13830  ghmgrp2  13851  ghmlin  13853  ghmnsgpreima  13874  kerf1ghm  13879  gsumsplit0  13951  srgdilem  14001  srgdir  14007  srgridm  14012  ringdilem  14044  ringdir  14051  ringridm  14056  unitmulcl  14146  unitnegcl  14163  rhmmhm  14192  elrhmunit  14210  lringuplu  14229  subrgring  14257  subrg1cl  14262  qusrhm  14561  znunit  14692  znrrg  14693  psrelbas  14708  mplsubgfilemcl  14732  mplsubgfileminv  14733  inopn  14746  restbasg  14911  ssrest  14925  cntop2  14945  icnpimaex  14954  cnima  14963  lmfss  14987  lmtopcnp  14993  txhmeo  15062  txswaphmeo  15064  psmet0  15070  psmettri2  15071  blhalf  15151  bdxmet  15244  xmetxpbl  15251  ioo2bl  15294  tgioo  15297  cncfi  15321  rescncf  15324  cdivcncfap  15347  cnopnap  15354  divcncfap  15357  dedekindeulemeu  15365  dedekindicclemeu  15374  ivthinclemum  15378  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthinclemdisj  15383  ivthdec  15387  ivthreinc  15388  limcimo  15408  cnplimcim  15410  cnplimclemr  15412  cnlimci  15416  limccnpcntop  15418  limccnp2lem  15419  limccnp2cntop  15420  limccoap  15421  reldvg  15422  dvbsssg  15429  dvfgg  15431  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  plyco  15502  plycj  15504  plyrecj  15506  sin0pilem1  15524  sin0pilem2  15525  tanrpcl  15580  tangtx  15581  cos0pilt1  15595  logbgcd1irraplemexp  15711  mpodvdsmulf1o  15733  perfect  15744  lgsne0  15786  lgseisen  15822  lgsquad2lem2  15830  2sqlem8a  15870  2sqlem8  15871  structgrssiedg  15913  uhgrm  15948  umgredgne  16020  usgruspgrben  16056  usgredgppren  16067  umgr2edg  16077  vtxdumgrfival  16168  wlkpropg  16194  wlkv  16196  wlkvtxeledgg  16214  g0wlk0  16240  trlsv  16254  clwwlknlen  16281  eupthv  16316  eupthf1o  16320  eupth2lem3lem4fi  16343  eulerpathprum  16350  bj-charfunbi  16457  bj-inf2vnlem1  16616  pwf1oexmid  16651  subctctexmid  16652  iooref1o  16689  taupi  16729  alsi2d  16748  alsc2d  16750