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  1787  eldifbd  3156  unssbd  3328  opth  4255  potr  4326  frind  4370  brrelex2  4685  funinsn  5284  feu  5417  fcnvres  5418  fun11iun  5501  elmpocl2  6092  oprssdmm  6195  tfrlem1  6332  tfrlemisucfn  6348  tfrlemisucaccv  6349  tfrlemibxssdm  6351  tfrlemibfn  6352  tfrlemi14d  6357  swoer  6586  elmapssres  6698  mapsspm  6707  pmsspw  6708  mapss  6716  dom0  6865  xpf1o  6871  sbthlemi8  6992  sbthlemi9  6993  supelti  7030  supisoti  7038  djulclb  7083  nnnninfeq2  7156  cardcl  7209  isnumi  7210  cardval3ex  7213  exmidonfinlem  7221  en2eleq  7223  acfun  7235  exmidaclem  7236  dftap2  7279  exmidapne  7288  ccfunen  7292  indpi  7370  dfplpq2  7382  ltbtwnnq  7444  enq0tr  7462  nqnq0pi  7466  elnp1st2nd  7504  prcunqu  7513  prnmaxl  7516  prloc  7519  genpcuu  7548  addnqprllem  7555  addlocprlemeq  7561  addlocprlemgt  7562  addlocpr  7564  nqprxx  7574  gtnqex  7578  appdivnq  7591  prmuloclemcalc  7593  prmuloc  7594  mullocprlem  7598  ltprordil  7617  ltnqpri  7622  ltexprlemm  7628  ltexprlemopl  7629  ltexprlemlol  7630  ltexprlemopu  7631  ltexprlemupu  7632  ltexprlemdisj  7634  ltexprlemloc  7635  ltexprlemfl  7637  ltexprlemrl  7638  ltexprlemfu  7639  ltexprlemru  7640  ltexpri  7641  recexprlemell  7650  recexprlemelu  7651  recexprlemloc  7659  recexprlempr  7660  recexprlem1ssl  7661  recexprlem1ssu  7662  recexprlemss1l  7663  aptipr  7669  cauappcvgprlemlol  7675  cauappcvgprlemupu  7677  cauappcvgprlemladdfu  7682  cauappcvgprlemladdfl  7683  cauappcvgprlemladdrl  7685  caucvgprlemnkj  7694  caucvgprlemnbj  7695  caucvgprlemlol  7698  caucvgprlemupu  7700  caucvgprlemladdfu  7705  caucvgprlem1  7707  caucvgprlem2  7708  caucvgprprlemnjltk  7719  caucvgprprlemnbj  7721  caucvgprprlemlol  7726  caucvgprprlemupu  7728  caucvgprprlemexbt  7734  caucvgprprlem1  7737  caucvgprprlem2  7738  suplocexprlemrl  7745  suplocexprlemru  7747  suplocexprlemdisj  7748  suplocexprlemub  7751  suplocexprlemlub  7752  ltsrprg  7775  gt0srpr  7776  recexgt0sr  7801  addgt0sr  7803  mulgt0sr  7806  map2psrprg  7833  suplocsrlemb  7834  suplocsrlem  7836  nnindnn  7921  axcaucvglemcau  7926  axpre-suploclemres  7929  apreap  8573  apreim  8589  mulge0  8605  apti  8608  mulap0bbd  8646  lble  8933  nnind  8964  recnz  9375  uzind  9393  eluzadd  9585  eluzsub  9586  ixxss1  9933  ixxss2  9934  ixxss12  9935  iccss2  9973  iccssioo2  9975  iccssico2  9976  elfzolt2  10185  ioom  10290  elicore  10296  flqltp1  10309  addmodlteq  10428  expcl2lemap  10562  expap0i  10582  hashennnuni  10790  crre  10897  caucvgre  11021  cvg1nlemcau  11024  cvg1nlemres  11025  resqrexlemoverl  11061  sqrtge0  11073  fimaxre2  11266  climi  11326  reccn2ap  11352  climge0  11364  nnf1o  11415  sumpr  11452  fsump1i  11472  fsum00  11501  fsumparts  11509  mertenslemi1  11574  addsin  11781  subsin  11782  addcos  11785  subcos  11786  sinbnd2  11793  cosbnd2  11794  dvdsaddre2b  11879  evenelz  11903  4dvdseven  11953  infssuzcldc  11983  gcd0id  12011  gcd1  12019  bezoutlemstep  12029  dvdsgcdb  12045  mulgcd  12048  gcdzeq  12054  dvdsmulgcd  12057  sqgcd  12061  dvdssqlem  12062  bezoutr  12064  uzwodc  12069  lcmval  12094  lcmcllem  12098  lcmgcdlem  12108  lcmdvds  12110  lcmgcdeq  12114  lcmdvdsb  12115  mulgcddvds  12125  rpmulgcd2  12126  qredeu  12128  rpdvds  12130  divgcdcoprm0  12132  isprm3  12149  divgcdodd  12174  coprm  12175  rpexp  12184  sqrt2irr  12193  qdencl  12220  qeqnumdivden  12225  divnumden  12227  divdenle  12228  densq  12235  phimullem  12256  eulerthlem1  12258  eulerthlemrprm  12260  eulerthlemth  12263  prmdiveq  12267  prmdivdiv  12268  hashgcdeq  12270  phisum  12271  odzid  12275  reumodprminv  12284  oddn2prm  12292  pythagtriplem4  12299  pythagtriplem11  12305  pythagtriplem13  12307  pythagtriplem19  12313  pclemub  12318  pcprendvds2  12322  pcpre1  12323  pcpremul  12324  pceulem  12325  pczdvds  12345  pc2dvds  12361  pcaddlem  12370  pcmpt  12374  pcmpt2  12375  pcmptdvds  12376  pcprod  12377  pockthlem  12387  pockthg  12388  prmunb  12393  1arithlem4  12397  4sqlem7  12415  4sqlem8  12416  4sqlem9  12417  4sqlem10  12418  4sqlemffi  12427  4sqlem15  12436  4sqlem16  12437  4sqlem17  12438  4sqlem18  12439  ennnfonelemom  12458  ennnfonelemex  12464  ennnfonelemf1  12468  ctiunctlemu1st  12484  ctiunctlemu2nd  12485  fnpr2ob  12813  mgmlrid  12852  mndrid  12894  grpinvcnv  13009  dfgrp3mlem  13039  eqglact  13161  ghmgrp2  13182  ghmlin  13184  ghmnsgpreima  13205  kerf1ghm  13210  srgdilem  13320  srgdir  13326  srgridm  13331  ringdilem  13363  ringdir  13370  ringridm  13375  unitmulcl  13460  unitnegcl  13477  rhmmhm  13506  elrhmunit  13524  lringuplu  13540  subrgring  13568  subrg1cl  13573  inopn  13955  restbasg  14120  ssrest  14134  cntop2  14154  icnpimaex  14163  cnima  14172  lmfss  14196  lmtopcnp  14202  txhmeo  14271  txswaphmeo  14273  psmet0  14279  psmettri2  14280  blhalf  14360  bdxmet  14453  xmetxpbl  14460  ioo2bl  14495  tgioo  14498  cncfi  14517  rescncf  14520  cdivcncfap  14539  cnopnap  14546  dedekindeulemeu  14552  dedekindicclemeu  14561  ivthinclemum  14565  ivthinclemlopn  14566  ivthinclemuopn  14568  ivthinclemdisj  14570  ivthdec  14574  limcimo  14586  cnplimcim  14588  cnplimclemr  14590  cnlimci  14594  limccnpcntop  14596  limccnp2lem  14597  limccnp2cntop  14598  limccoap  14599  reldvg  14600  dvbsssg  14607  dvfgg  14609  dvaddxxbr  14617  dvmulxxbr  14618  dvcoapbr  14623  dvcjbr  14624  dvrecap  14629  sin0pilem1  14654  sin0pilem2  14655  tanrpcl  14710  tangtx  14711  cos0pilt1  14725  logbgcd1irraplemexp  14838  lgsne0  14892  2sqlem8a  14922  2sqlem8  14923  bj-charfunbi  15016  bj-inf2vnlem1  15175  pwf1oexmid  15203  subctctexmid  15204  iooref1o  15236  taupi  15275  alsi2d  15284  alsc2d  15286