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  1001  simp3  1002  sbh  1800  eldifbd  3182  unssbd  3355  opth  4294  potr  4368  frind  4412  brrelex2  4729  funinsn  5337  feu  5475  fcnvres  5476  fun11iun  5560  funopsn  5780  elmpocl2  6161  uchoice  6241  oprssdmm  6275  tfrlem1  6412  tfrlemisucfn  6428  tfrlemisucaccv  6429  tfrlemibxssdm  6431  tfrlemibfn  6432  tfrlemi14d  6437  swoer  6666  elmapssres  6778  mapsspm  6787  pmsspw  6788  mapss  6796  dom0  6955  xpf1o  6961  sbthlemi8  7087  sbthlemi9  7088  supelti  7125  supisoti  7133  djulclb  7178  nninfninc  7246  nnnninfeq2  7252  cardcl  7309  isnumi  7310  cardval3ex  7313  exmidonfinlem  7327  en2eleq  7329  finacn  7342  acfun  7345  exmidaclem  7346  pw1if  7366  dftap2  7393  exmidapne  7402  ccfunen  7406  acnccim  7414  indpi  7485  dfplpq2  7497  ltbtwnnq  7559  enq0tr  7577  nqnq0pi  7581  elnp1st2nd  7619  prcunqu  7628  prnmaxl  7631  prloc  7634  genpcuu  7663  addnqprllem  7670  addlocprlemeq  7676  addlocprlemgt  7677  addlocpr  7679  nqprxx  7689  gtnqex  7693  appdivnq  7706  prmuloclemcalc  7708  prmuloc  7709  mullocprlem  7713  ltprordil  7732  ltnqpri  7737  ltexprlemm  7743  ltexprlemopl  7744  ltexprlemlol  7745  ltexprlemopu  7746  ltexprlemupu  7747  ltexprlemdisj  7749  ltexprlemloc  7750  ltexprlemfl  7752  ltexprlemrl  7753  ltexprlemfu  7754  ltexprlemru  7755  ltexpri  7756  recexprlemell  7765  recexprlemelu  7766  recexprlemloc  7774  recexprlempr  7775  recexprlem1ssl  7776  recexprlem1ssu  7777  recexprlemss1l  7778  aptipr  7784  cauappcvgprlemlol  7790  cauappcvgprlemupu  7792  cauappcvgprlemladdfu  7797  cauappcvgprlemladdfl  7798  cauappcvgprlemladdrl  7800  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprlemlol  7813  caucvgprlemupu  7815  caucvgprlemladdfu  7820  caucvgprlem1  7822  caucvgprlem2  7823  caucvgprprlemnjltk  7834  caucvgprprlemnbj  7836  caucvgprprlemlol  7841  caucvgprprlemupu  7843  caucvgprprlemexbt  7849  caucvgprprlem1  7852  caucvgprprlem2  7853  suplocexprlemrl  7860  suplocexprlemru  7862  suplocexprlemdisj  7863  suplocexprlemub  7866  suplocexprlemlub  7867  ltsrprg  7890  gt0srpr  7891  recexgt0sr  7916  addgt0sr  7918  mulgt0sr  7921  map2psrprg  7948  suplocsrlemb  7949  suplocsrlem  7951  nnindnn  8036  axcaucvglemcau  8041  axpre-suploclemres  8044  apreap  8690  apreim  8706  mulge0  8722  apti  8725  mulap0bbd  8763  lble  9050  nnind  9082  recnz  9496  uzind  9514  eluzadd  9707  eluzsub  9708  ixxss1  10056  ixxss2  10057  ixxss12  10058  iccss2  10096  iccssioo2  10098  iccssico2  10099  elfzolt2  10309  infssuzcldc  10410  ioom  10435  elicore  10441  flqltp1  10454  addmodlteq  10575  expcl2lemap  10728  expap0i  10748  hashennnuni  10956  hashdmprop2dom  11021  wrdexb  11038  swrdsbslen  11152  swrdspsleq  11153  crre  11253  caucvgre  11377  cvg1nlemcau  11380  cvg1nlemres  11381  resqrexlemoverl  11417  sqrtge0  11429  fimaxre2  11623  climi  11683  reccn2ap  11709  climge0  11721  nnf1o  11772  sumpr  11809  fsump1i  11829  fsum00  11858  fsumparts  11866  mertenslemi1  11931  addsin  12138  subsin  12139  addcos  12142  subcos  12143  sinbnd2  12150  cosbnd2  12151  sinltxirr  12157  dvdsaddre2b  12237  evenelz  12263  4dvdseven  12313  gcd0id  12385  gcd1  12393  bezoutlemstep  12403  dvdsgcdb  12419  mulgcd  12422  gcdzeq  12428  dvdsmulgcd  12431  sqgcd  12435  dvdssqlem  12436  bezoutr  12438  uzwodc  12443  nninfctlemfo  12446  lcmval  12470  lcmcllem  12474  lcmgcdlem  12484  lcmdvds  12486  lcmgcdeq  12490  lcmdvdsb  12491  mulgcddvds  12501  rpmulgcd2  12502  qredeu  12504  rpdvds  12506  divgcdcoprm0  12508  isprm3  12525  divgcdodd  12550  coprm  12551  rpexp  12560  sqrt2irr  12569  qdencl  12596  qeqnumdivden  12601  divnumden  12603  divdenle  12604  densq  12611  phimullem  12632  eulerthlem1  12634  eulerthlemrprm  12636  eulerthlemth  12639  prmdiveq  12643  prmdivdiv  12644  hashgcdeq  12647  phisum  12648  odzid  12652  reumodprminv  12661  oddn2prm  12669  pythagtriplem4  12676  pythagtriplem11  12682  pythagtriplem13  12684  pythagtriplem19  12690  pclemub  12695  pcprendvds2  12699  pcpre1  12700  pcpremul  12701  pceulem  12702  pczdvds  12722  pc2dvds  12738  pcaddlem  12747  pcmpt  12751  pcmpt2  12752  pcmptdvds  12753  pcprod  12754  pockthlem  12764  pockthg  12765  prmunb  12770  1arithlem4  12774  4sqlem7  12792  4sqlem8  12793  4sqlem9  12794  4sqlem10  12795  4sqlemffi  12804  4sqlem15  12813  4sqlem16  12814  4sqlem17  12815  4sqlem18  12816  ennnfonelemom  12864  ennnfonelemex  12870  ennnfonelemf1  12874  ctiunctlemu1st  12890  ctiunctlemu2nd  12891  fnpr2ob  13257  mgmlrid  13296  gsumfzval  13308  gsumval2  13314  mndrid  13353  prdsmndd  13365  grpinvcnv  13485  dfgrp3mlem  13515  prdsgrpd  13526  prdsinvgd  13527  eqglact  13646  ghmgrp2  13667  ghmlin  13669  ghmnsgpreima  13690  kerf1ghm  13695  srgdilem  13816  srgdir  13822  srgridm  13827  ringdilem  13859  ringdir  13866  ringridm  13871  unitmulcl  13960  unitnegcl  13977  rhmmhm  14006  elrhmunit  14024  lringuplu  14043  subrgring  14071  subrg1cl  14076  qusrhm  14375  znunit  14506  znrrg  14507  psrelbas  14522  mplsubgfilemcl  14546  mplsubgfileminv  14547  inopn  14560  restbasg  14725  ssrest  14739  cntop2  14759  icnpimaex  14768  cnima  14777  lmfss  14801  lmtopcnp  14807  txhmeo  14876  txswaphmeo  14878  psmet0  14884  psmettri2  14885  blhalf  14965  bdxmet  15058  xmetxpbl  15065  ioo2bl  15108  tgioo  15111  cncfi  15135  rescncf  15138  cdivcncfap  15161  cnopnap  15168  divcncfap  15171  dedekindeulemeu  15179  dedekindicclemeu  15188  ivthinclemum  15192  ivthinclemlopn  15193  ivthinclemuopn  15195  ivthinclemdisj  15197  ivthdec  15201  ivthreinc  15202  limcimo  15222  cnplimcim  15224  cnplimclemr  15226  cnlimci  15230  limccnpcntop  15232  limccnp2lem  15233  limccnp2cntop  15234  limccoap  15235  reldvg  15236  dvbsssg  15243  dvfgg  15245  dvaddxxbr  15258  dvmulxxbr  15259  dvcoapbr  15264  dvcjbr  15265  dvrecap  15270  plyco  15316  plycj  15318  plyrecj  15320  sin0pilem1  15338  sin0pilem2  15339  tanrpcl  15394  tangtx  15395  cos0pilt1  15409  logbgcd1irraplemexp  15525  mpodvdsmulf1o  15547  perfect  15558  lgsne0  15600  lgseisen  15636  lgsquad2lem2  15644  2sqlem8a  15684  2sqlem8  15685  structgrssiedg  15727  uhgrm  15759  umgredgne  15824  bj-charfunbi  15916  bj-inf2vnlem1  16075  pwf1oexmid  16108  subctctexmid  16109  iooref1o  16145  taupi  16184  alsi2d  16193  alsc2d  16195