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  simprld  530  simprrd  532  simp2  1022  simp3  1023  sbh  1822  eldifbd  3209  unssbd  3382  opth  4323  potr  4399  frind  4443  brrelex2  4760  funinsn  5370  feu  5510  fcnvres  5511  fun11iun  5595  funopsn  5819  elmpocl2  6208  uchoice  6289  oprssdmm  6323  tfrlem1  6460  tfrlemisucfn  6476  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemi14d  6485  swoer  6716  elmapssres  6828  mapsspm  6837  pmsspw  6838  mapss  6846  dom0  7007  xpf1o  7013  sbthlemi8  7142  sbthlemi9  7143  supelti  7180  supisoti  7188  djulclb  7233  nninfninc  7301  nnnninfeq2  7307  cardcl  7364  isnumi  7365  cardval3ex  7368  exmidonfinlem  7382  en2eleq  7384  finacn  7397  acfun  7400  exmidaclem  7401  pw1if  7421  dftap2  7448  exmidapne  7457  ccfunen  7461  acnccim  7469  indpi  7540  dfplpq2  7552  ltbtwnnq  7614  enq0tr  7632  nqnq0pi  7636  elnp1st2nd  7674  prcunqu  7683  prnmaxl  7686  prloc  7689  genpcuu  7718  addnqprllem  7725  addlocprlemeq  7731  addlocprlemgt  7732  addlocpr  7734  nqprxx  7744  gtnqex  7748  appdivnq  7761  prmuloclemcalc  7763  prmuloc  7764  mullocprlem  7768  ltprordil  7787  ltnqpri  7792  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  ltexpri  7811  recexprlemell  7820  recexprlemelu  7821  recexprlemloc  7829  recexprlempr  7830  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  aptipr  7839  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdrl  7855  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprlemladdfu  7875  caucvgprlem1  7877  caucvgprlem2  7878  caucvgprprlemnjltk  7889  caucvgprprlemnbj  7891  caucvgprprlemlol  7896  caucvgprprlemupu  7898  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  suplocexprlemrl  7915  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemub  7921  suplocexprlemlub  7922  ltsrprg  7945  gt0srpr  7946  recexgt0sr  7971  addgt0sr  7973  mulgt0sr  7976  map2psrprg  8003  suplocsrlemb  8004  suplocsrlem  8006  nnindnn  8091  axcaucvglemcau  8096  axpre-suploclemres  8099  apreap  8745  apreim  8761  mulge0  8777  apti  8780  mulap0bbd  8818  lble  9105  nnind  9137  recnz  9551  uzind  9569  eluzadd  9763  eluzsub  9764  ixxss1  10112  ixxss2  10113  ixxss12  10114  iccss2  10152  iccssioo2  10154  iccssico2  10155  elfzolt2  10365  infssuzcldc  10467  ioom  10492  elicore  10498  flqltp1  10511  addmodlteq  10632  expcl2lemap  10785  expap0i  10805  hashennnuni  11013  hashdmprop2dom  11079  wrdexb  11096  swrdsbslen  11213  swrdspsleq  11214  crre  11383  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemoverl  11547  sqrtge0  11559  fimaxre2  11753  climi  11813  reccn2ap  11839  climge0  11851  nnf1o  11902  sumpr  11939  fsump1i  11959  fsum00  11988  fsumparts  11996  mertenslemi1  12061  addsin  12268  subsin  12269  addcos  12272  subcos  12273  sinbnd2  12280  cosbnd2  12281  sinltxirr  12287  dvdsaddre2b  12367  evenelz  12393  4dvdseven  12443  gcd0id  12515  gcd1  12523  bezoutlemstep  12533  dvdsgcdb  12549  mulgcd  12552  gcdzeq  12558  dvdsmulgcd  12561  sqgcd  12565  dvdssqlem  12566  bezoutr  12568  uzwodc  12573  nninfctlemfo  12576  lcmval  12600  lcmcllem  12604  lcmgcdlem  12614  lcmdvds  12616  lcmgcdeq  12620  lcmdvdsb  12621  mulgcddvds  12631  rpmulgcd2  12632  qredeu  12634  rpdvds  12636  divgcdcoprm0  12638  isprm3  12655  divgcdodd  12680  coprm  12681  rpexp  12690  sqrt2irr  12699  qdencl  12726  qeqnumdivden  12731  divnumden  12733  divdenle  12734  densq  12741  phimullem  12762  eulerthlem1  12764  eulerthlemrprm  12766  eulerthlemth  12769  prmdiveq  12773  prmdivdiv  12774  hashgcdeq  12777  phisum  12778  odzid  12782  reumodprminv  12791  oddn2prm  12799  pythagtriplem4  12806  pythagtriplem11  12812  pythagtriplem13  12814  pythagtriplem19  12820  pclemub  12825  pcprendvds2  12829  pcpre1  12830  pcpremul  12831  pceulem  12832  pczdvds  12852  pc2dvds  12868  pcaddlem  12877  pcmpt  12881  pcmpt2  12882  pcmptdvds  12883  pcprod  12884  pockthlem  12894  pockthg  12895  prmunb  12900  1arithlem4  12904  4sqlem7  12922  4sqlem8  12923  4sqlem9  12924  4sqlem10  12925  4sqlemffi  12934  4sqlem15  12943  4sqlem16  12944  4sqlem17  12945  4sqlem18  12946  ennnfonelemom  12994  ennnfonelemex  13000  ennnfonelemf1  13004  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  fnpr2ob  13388  mgmlrid  13427  gsumfzval  13439  gsumval2  13445  mndrid  13484  prdsmndd  13496  grpinvcnv  13616  dfgrp3mlem  13646  prdsgrpd  13657  prdsinvgd  13658  eqglact  13777  ghmgrp2  13798  ghmlin  13800  ghmnsgpreima  13821  kerf1ghm  13826  srgdilem  13947  srgdir  13953  srgridm  13958  ringdilem  13990  ringdir  13997  ringridm  14002  unitmulcl  14092  unitnegcl  14109  rhmmhm  14138  elrhmunit  14156  lringuplu  14175  subrgring  14203  subrg1cl  14208  qusrhm  14507  znunit  14638  znrrg  14639  psrelbas  14654  mplsubgfilemcl  14678  mplsubgfileminv  14679  inopn  14692  restbasg  14857  ssrest  14871  cntop2  14891  icnpimaex  14900  cnima  14909  lmfss  14933  lmtopcnp  14939  txhmeo  15008  txswaphmeo  15010  psmet0  15016  psmettri2  15017  blhalf  15097  bdxmet  15190  xmetxpbl  15197  ioo2bl  15240  tgioo  15243  cncfi  15267  rescncf  15270  cdivcncfap  15293  cnopnap  15300  divcncfap  15303  dedekindeulemeu  15311  dedekindicclemeu  15320  ivthinclemum  15324  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthinclemdisj  15329  ivthdec  15333  ivthreinc  15334  limcimo  15354  cnplimcim  15356  cnplimclemr  15358  cnlimci  15362  limccnpcntop  15364  limccnp2lem  15365  limccnp2cntop  15366  limccoap  15367  reldvg  15368  dvbsssg  15375  dvfgg  15377  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvrecap  15402  plyco  15448  plycj  15450  plyrecj  15452  sin0pilem1  15470  sin0pilem2  15471  tanrpcl  15526  tangtx  15527  cos0pilt1  15541  logbgcd1irraplemexp  15657  mpodvdsmulf1o  15679  perfect  15690  lgsne0  15732  lgseisen  15768  lgsquad2lem2  15776  2sqlem8a  15816  2sqlem8  15817  structgrssiedg  15859  uhgrm  15893  umgredgne  15963  usgruspgrben  15999  usgredgppren  16010  umgr2edg  16020  vtxdumgrfival  16057  wlkpropg  16065  wlkv  16067  wlkvtxeledgg  16085  g0wlk0  16111  trlsv  16123  bj-charfunbi  16229  bj-inf2vnlem1  16388  pwf1oexmid  16424  subctctexmid  16425  iooref1o  16462  taupi  16501  alsi2d  16510  alsc2d  16512