Theorem simprd 113

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 109	. 2 |- ( ( ps /\ ch ) -> ch )
3	1, 2	syl 14	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106

This theorem is referenced by:  biimpr  129  simprbi  273  simplbda  382  simp2  993  simp3  994  sbh  1769  eldifbd  3133  unssbd  3305  opth  4222  potr  4293  frind  4337  brrelex2  4652  funinsn  5247  feu  5380  fcnvres  5381  fun11iun  5463  elmpocl2  6049  oprssdmm  6150  tfrlem1  6287  tfrlemisucfn  6303  tfrlemisucaccv  6304  tfrlemibxssdm  6306  tfrlemibfn  6307  tfrlemi14d  6312  swoer  6541  elmapssres  6651  mapsspm  6660  pmsspw  6661  mapss  6669  dom0  6816  xpf1o  6822  sbthlemi8  6941  sbthlemi9  6942  supelti  6979  supisoti  6987  djulclb  7032  nnnninfeq2  7105  cardcl  7158  isnumi  7159  cardval3ex  7162  exmidonfinlem  7170  en2eleq  7172  acfun  7184  exmidaclem  7185  ccfunen  7226  indpi  7304  dfplpq2  7316  ltbtwnnq  7378  enq0tr  7396  nqnq0pi  7400  elnp1st2nd  7438  prcunqu  7447  prnmaxl  7450  prloc  7453  genpcuu  7482  addnqprllem  7489  addlocprlemeq  7495  addlocprlemgt  7496  addlocpr  7498  nqprxx  7508  gtnqex  7512  appdivnq  7525  prmuloclemcalc  7527  prmuloc  7528  mullocprlem  7532  ltprordil  7551  ltnqpri  7556  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemfl  7571  ltexprlemrl  7572  ltexprlemfu  7573  ltexprlemru  7574  ltexpri  7575  recexprlemell  7584  recexprlemelu  7585  recexprlemloc  7593  recexprlempr  7594  recexprlem1ssl  7595  recexprlem1ssu  7596  recexprlemss1l  7597  aptipr  7603  cauappcvgprlemlol  7609  cauappcvgprlemupu  7611  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdrl  7619  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemlol  7632  caucvgprlemupu  7634  caucvgprlemladdfu  7639  caucvgprlem1  7641  caucvgprlem2  7642  caucvgprprlemnjltk  7653  caucvgprprlemnbj  7655  caucvgprprlemlol  7660  caucvgprprlemupu  7662  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  suplocexprlemrl  7679  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemub  7685  suplocexprlemlub  7686  ltsrprg  7709  gt0srpr  7710  recexgt0sr  7735  addgt0sr  7737  mulgt0sr  7740  map2psrprg  7767  suplocsrlemb  7768  suplocsrlem  7770  nnindnn  7855  axcaucvglemcau  7860  axpre-suploclemres  7863  apreap  8506  apreim  8522  mulge0  8538  apti  8541  mulap0bbd  8578  lble  8863  nnind  8894  recnz  9305  uzind  9323  eluzadd  9515  eluzsub  9516  ixxss1  9861  ixxss2  9862  ixxss12  9863  iccss2  9901  iccssioo2  9903  iccssico2  9904  elfzolt2  10112  ioom  10217  elicore  10223  flqltp1  10235  addmodlteq  10354  expcl2lemap  10488  expap0i  10508  hashennnuni  10713  crre  10821  caucvgre  10945  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemoverl  10985  sqrtge0  10997  fimaxre2  11190  climi  11250  reccn2ap  11276  climge0  11288  nnf1o  11339  sumpr  11376  fsump1i  11396  fsum00  11425  fsumparts  11433  mertenslemi1  11498  addsin  11705  subsin  11706  addcos  11709  subcos  11710  sinbnd2  11717  cosbnd2  11718  evenelz  11826  4dvdseven  11876  infssuzcldc  11906  gcd0id  11934  gcd1  11942  bezoutlemstep  11952  dvdsgcdb  11968  mulgcd  11971  gcdzeq  11977  dvdsmulgcd  11980  sqgcd  11984  dvdssqlem  11985  bezoutr  11987  uzwodc  11992  lcmval  12017  lcmcllem  12021  lcmgcdlem  12031  lcmdvds  12033  lcmgcdeq  12037  lcmdvdsb  12038  mulgcddvds  12048  rpmulgcd2  12049  qredeu  12051  rpdvds  12053  divgcdcoprm0  12055  isprm3  12072  divgcdodd  12097  coprm  12098  rpexp  12107  sqrt2irr  12116  qdencl  12143  qeqnumdivden  12148  divnumden  12150  divdenle  12151  densq  12158  phimullem  12179  eulerthlem1  12181  eulerthlemrprm  12183  eulerthlemth  12186  prmdiveq  12190  prmdivdiv  12191  hashgcdeq  12193  phisum  12194  odzid  12198  reumodprminv  12207  oddn2prm  12215  pythagtriplem4  12222  pythagtriplem11  12228  pythagtriplem13  12230  pythagtriplem19  12236  pclemub  12241  pcprendvds2  12245  pcpre1  12246  pcpremul  12247  pceulem  12248  pczdvds  12267  pc2dvds  12283  pcaddlem  12292  pcmpt  12295  pcmpt2  12296  pcmptdvds  12297  pcprod  12298  pockthlem  12308  pockthg  12309  prmunb  12314  1arithlem4  12318  4sqlem7  12336  4sqlem8  12337  4sqlem9  12338  4sqlem10  12339  ennnfonelemom  12363  ennnfonelemex  12369  ennnfonelemf1  12373  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  mgmlrid  12633  mndrid  12672  grpinvcnv  12767  inopn  12795  restbasg  12962  ssrest  12976  cntop2  12996  icnpimaex  13005  cnima  13014  lmfss  13038  lmtopcnp  13044  txhmeo  13113  txswaphmeo  13115  psmet0  13121  psmettri2  13122  blhalf  13202  bdxmet  13295  xmetxpbl  13302  ioo2bl  13337  tgioo  13340  cncfi  13359  rescncf  13362  cdivcncfap  13381  cnopnap  13388  dedekindeulemeu  13394  dedekindicclemeu  13403  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinclemdisj  13412  ivthdec  13416  limcimo  13428  cnplimcim  13430  cnplimclemr  13432  cnlimci  13436  limccnpcntop  13438  limccnp2lem  13439  limccnp2cntop  13440  limccoap  13441  reldvg  13442  dvbsssg  13449  dvfgg  13451  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  sin0pilem1  13496  sin0pilem2  13497  tanrpcl  13552  tangtx  13553  cos0pilt1  13567  logbgcd1irraplemexp  13680  lgsne0  13733  2sqlem8a  13752  2sqlem8  13753  bj-charfunbi  13846  bj-inf2vnlem1  14005  pwf1oexmid  14032  subctctexmid  14034  iooref1o  14066  taupi  14102  alsi2d  14111  alsc2d  14113