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  1000  simp3  1001  sbh  1790  eldifbd  3169  unssbd  3341  opth  4270  potr  4343  frind  4387  brrelex2  4704  funinsn  5307  feu  5440  fcnvres  5441  fun11iun  5525  elmpocl2  6120  uchoice  6195  oprssdmm  6229  tfrlem1  6366  tfrlemisucfn  6382  tfrlemisucaccv  6383  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemi14d  6391  swoer  6620  elmapssres  6732  mapsspm  6741  pmsspw  6742  mapss  6750  dom0  6899  xpf1o  6905  sbthlemi8  7030  sbthlemi9  7031  supelti  7068  supisoti  7076  djulclb  7121  nninfninc  7189  nnnninfeq2  7195  cardcl  7248  isnumi  7249  cardval3ex  7252  exmidonfinlem  7260  en2eleq  7262  acfun  7274  exmidaclem  7275  dftap2  7318  exmidapne  7327  ccfunen  7331  indpi  7409  dfplpq2  7421  ltbtwnnq  7483  enq0tr  7501  nqnq0pi  7505  elnp1st2nd  7543  prcunqu  7552  prnmaxl  7555  prloc  7558  genpcuu  7587  addnqprllem  7594  addlocprlemeq  7600  addlocprlemgt  7601  addlocpr  7603  nqprxx  7613  gtnqex  7617  appdivnq  7630  prmuloclemcalc  7632  prmuloc  7633  mullocprlem  7637  ltprordil  7656  ltnqpri  7661  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  ltexpri  7680  recexprlemell  7689  recexprlemelu  7690  recexprlemloc  7698  recexprlempr  7699  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  aptipr  7708  cauappcvgprlemlol  7714  cauappcvgprlemupu  7716  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdrl  7724  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemlol  7737  caucvgprlemupu  7739  caucvgprlemladdfu  7744  caucvgprlem1  7746  caucvgprlem2  7747  caucvgprprlemnjltk  7758  caucvgprprlemnbj  7760  caucvgprprlemlol  7765  caucvgprprlemupu  7767  caucvgprprlemexbt  7773  caucvgprprlem1  7776  caucvgprprlem2  7777  suplocexprlemrl  7784  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemub  7790  suplocexprlemlub  7791  ltsrprg  7814  gt0srpr  7815  recexgt0sr  7840  addgt0sr  7842  mulgt0sr  7845  map2psrprg  7872  suplocsrlemb  7873  suplocsrlem  7875  nnindnn  7960  axcaucvglemcau  7965  axpre-suploclemres  7968  apreap  8614  apreim  8630  mulge0  8646  apti  8649  mulap0bbd  8687  lble  8974  nnind  9006  recnz  9419  uzind  9437  eluzadd  9630  eluzsub  9631  ixxss1  9979  ixxss2  9980  ixxss12  9981  iccss2  10019  iccssioo2  10021  iccssico2  10022  elfzolt2  10232  infssuzcldc  10325  ioom  10350  elicore  10356  flqltp1  10369  addmodlteq  10490  expcl2lemap  10643  expap0i  10663  hashennnuni  10871  wrdexb  10947  crre  11022  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemoverl  11186  sqrtge0  11198  fimaxre2  11392  climi  11452  reccn2ap  11478  climge0  11490  nnf1o  11541  sumpr  11578  fsump1i  11598  fsum00  11627  fsumparts  11635  mertenslemi1  11700  addsin  11907  subsin  11908  addcos  11911  subcos  11912  sinbnd2  11919  cosbnd2  11920  sinltxirr  11926  dvdsaddre2b  12006  evenelz  12032  4dvdseven  12082  gcd0id  12146  gcd1  12154  bezoutlemstep  12164  dvdsgcdb  12180  mulgcd  12183  gcdzeq  12189  dvdsmulgcd  12192  sqgcd  12196  dvdssqlem  12197  bezoutr  12199  uzwodc  12204  nninfctlemfo  12207  lcmval  12231  lcmcllem  12235  lcmgcdlem  12245  lcmdvds  12247  lcmgcdeq  12251  lcmdvdsb  12252  mulgcddvds  12262  rpmulgcd2  12263  qredeu  12265  rpdvds  12267  divgcdcoprm0  12269  isprm3  12286  divgcdodd  12311  coprm  12312  rpexp  12321  sqrt2irr  12330  qdencl  12357  qeqnumdivden  12362  divnumden  12364  divdenle  12365  densq  12372  phimullem  12393  eulerthlem1  12395  eulerthlemrprm  12397  eulerthlemth  12400  prmdiveq  12404  prmdivdiv  12405  hashgcdeq  12408  phisum  12409  odzid  12413  reumodprminv  12422  oddn2prm  12430  pythagtriplem4  12437  pythagtriplem11  12443  pythagtriplem13  12445  pythagtriplem19  12451  pclemub  12456  pcprendvds2  12460  pcpre1  12461  pcpremul  12462  pceulem  12463  pczdvds  12483  pc2dvds  12499  pcaddlem  12508  pcmpt  12512  pcmpt2  12513  pcmptdvds  12514  pcprod  12515  pockthlem  12525  pockthg  12526  prmunb  12531  1arithlem4  12535  4sqlem7  12553  4sqlem8  12554  4sqlem9  12555  4sqlem10  12556  4sqlemffi  12565  4sqlem15  12574  4sqlem16  12575  4sqlem17  12576  4sqlem18  12577  ennnfonelemom  12625  ennnfonelemex  12631  ennnfonelemf1  12635  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  fnpr2ob  12983  mgmlrid  13022  gsumfzval  13034  gsumval2  13040  mndrid  13077  grpinvcnv  13200  dfgrp3mlem  13230  eqglact  13355  ghmgrp2  13376  ghmlin  13378  ghmnsgpreima  13399  kerf1ghm  13404  srgdilem  13525  srgdir  13531  srgridm  13536  ringdilem  13568  ringdir  13575  ringridm  13580  unitmulcl  13669  unitnegcl  13686  rhmmhm  13715  elrhmunit  13733  lringuplu  13752  subrgring  13780  subrg1cl  13785  qusrhm  14084  znunit  14215  znrrg  14216  psrelbas  14228  inopn  14239  restbasg  14404  ssrest  14418  cntop2  14438  icnpimaex  14447  cnima  14456  lmfss  14480  lmtopcnp  14486  txhmeo  14555  txswaphmeo  14557  psmet0  14563  psmettri2  14564  blhalf  14644  bdxmet  14737  xmetxpbl  14744  ioo2bl  14787  tgioo  14790  cncfi  14814  rescncf  14817  cdivcncfap  14840  cnopnap  14847  divcncfap  14850  dedekindeulemeu  14858  dedekindicclemeu  14867  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthinclemdisj  14876  ivthdec  14880  ivthreinc  14881  limcimo  14901  cnplimcim  14903  cnplimclemr  14905  cnlimci  14909  limccnpcntop  14911  limccnp2lem  14912  limccnp2cntop  14913  limccoap  14914  reldvg  14915  dvbsssg  14922  dvfgg  14924  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  plyco  14995  plycj  14997  plyrecj  14999  sin0pilem1  15017  sin0pilem2  15018  tanrpcl  15073  tangtx  15074  cos0pilt1  15088  logbgcd1irraplemexp  15204  mpodvdsmulf1o  15226  perfect  15237  lgsne0  15279  lgseisen  15315  lgsquad2lem2  15323  2sqlem8a  15363  2sqlem8  15364  bj-charfunbi  15457  bj-inf2vnlem1  15616  pwf1oexmid  15644  subctctexmid  15645  iooref1o  15678  taupi  15717  alsi2d  15726  alsc2d  15728