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  1799  eldifbd  3178  unssbd  3351  opth  4281  potr  4355  frind  4399  brrelex2  4716  funinsn  5323  feu  5458  fcnvres  5459  fun11iun  5543  funopsn  5762  elmpocl2  6143  uchoice  6223  oprssdmm  6257  tfrlem1  6394  tfrlemisucfn  6410  tfrlemisucaccv  6411  tfrlemibxssdm  6413  tfrlemibfn  6414  tfrlemi14d  6419  swoer  6648  elmapssres  6760  mapsspm  6769  pmsspw  6770  mapss  6778  dom0  6935  xpf1o  6941  sbthlemi8  7066  sbthlemi9  7067  supelti  7104  supisoti  7112  djulclb  7157  nninfninc  7225  nnnninfeq2  7231  cardcl  7288  isnumi  7289  cardval3ex  7292  exmidonfinlem  7301  en2eleq  7303  finacn  7316  acfun  7319  exmidaclem  7320  dftap2  7363  exmidapne  7372  ccfunen  7376  acnccim  7384  indpi  7455  dfplpq2  7467  ltbtwnnq  7529  enq0tr  7547  nqnq0pi  7551  elnp1st2nd  7589  prcunqu  7598  prnmaxl  7601  prloc  7604  genpcuu  7633  addnqprllem  7640  addlocprlemeq  7646  addlocprlemgt  7647  addlocpr  7649  nqprxx  7659  gtnqex  7663  appdivnq  7676  prmuloclemcalc  7678  prmuloc  7679  mullocprlem  7683  ltprordil  7702  ltnqpri  7707  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  ltexpri  7726  recexprlemell  7735  recexprlemelu  7736  recexprlemloc  7744  recexprlempr  7745  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  aptipr  7754  cauappcvgprlemlol  7760  cauappcvgprlemupu  7762  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdrl  7770  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemlol  7783  caucvgprlemupu  7785  caucvgprlemladdfu  7790  caucvgprlem1  7792  caucvgprlem2  7793  caucvgprprlemnjltk  7804  caucvgprprlemnbj  7806  caucvgprprlemlol  7811  caucvgprprlemupu  7813  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  suplocexprlemrl  7830  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemub  7836  suplocexprlemlub  7837  ltsrprg  7860  gt0srpr  7861  recexgt0sr  7886  addgt0sr  7888  mulgt0sr  7891  map2psrprg  7918  suplocsrlemb  7919  suplocsrlem  7921  nnindnn  8006  axcaucvglemcau  8011  axpre-suploclemres  8014  apreap  8660  apreim  8676  mulge0  8692  apti  8695  mulap0bbd  8733  lble  9020  nnind  9052  recnz  9466  uzind  9484  eluzadd  9677  eluzsub  9678  ixxss1  10026  ixxss2  10027  ixxss12  10028  iccss2  10066  iccssioo2  10068  iccssico2  10069  elfzolt2  10279  infssuzcldc  10378  ioom  10403  elicore  10409  flqltp1  10422  addmodlteq  10543  expcl2lemap  10696  expap0i  10716  hashennnuni  10924  hashdmprop2dom  10989  wrdexb  11006  swrdsbslen  11119  swrdspsleq  11120  crre  11168  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemoverl  11332  sqrtge0  11344  fimaxre2  11538  climi  11598  reccn2ap  11624  climge0  11636  nnf1o  11687  sumpr  11724  fsump1i  11744  fsum00  11773  fsumparts  11781  mertenslemi1  11846  addsin  12053  subsin  12054  addcos  12057  subcos  12058  sinbnd2  12065  cosbnd2  12066  sinltxirr  12072  dvdsaddre2b  12152  evenelz  12178  4dvdseven  12228  gcd0id  12300  gcd1  12308  bezoutlemstep  12318  dvdsgcdb  12334  mulgcd  12337  gcdzeq  12343  dvdsmulgcd  12346  sqgcd  12350  dvdssqlem  12351  bezoutr  12353  uzwodc  12358  nninfctlemfo  12361  lcmval  12385  lcmcllem  12389  lcmgcdlem  12399  lcmdvds  12401  lcmgcdeq  12405  lcmdvdsb  12406  mulgcddvds  12416  rpmulgcd2  12417  qredeu  12419  rpdvds  12421  divgcdcoprm0  12423  isprm3  12440  divgcdodd  12465  coprm  12466  rpexp  12475  sqrt2irr  12484  qdencl  12511  qeqnumdivden  12516  divnumden  12518  divdenle  12519  densq  12526  phimullem  12547  eulerthlem1  12549  eulerthlemrprm  12551  eulerthlemth  12554  prmdiveq  12558  prmdivdiv  12559  hashgcdeq  12562  phisum  12563  odzid  12567  reumodprminv  12576  oddn2prm  12584  pythagtriplem4  12591  pythagtriplem11  12597  pythagtriplem13  12599  pythagtriplem19  12605  pclemub  12610  pcprendvds2  12614  pcpre1  12615  pcpremul  12616  pceulem  12617  pczdvds  12637  pc2dvds  12653  pcaddlem  12662  pcmpt  12666  pcmpt2  12667  pcmptdvds  12668  pcprod  12669  pockthlem  12679  pockthg  12680  prmunb  12685  1arithlem4  12689  4sqlem7  12707  4sqlem8  12708  4sqlem9  12709  4sqlem10  12710  4sqlemffi  12719  4sqlem15  12728  4sqlem16  12729  4sqlem17  12730  4sqlem18  12731  ennnfonelemom  12779  ennnfonelemex  12785  ennnfonelemf1  12789  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  fnpr2ob  13172  mgmlrid  13211  gsumfzval  13223  gsumval2  13229  mndrid  13268  prdsmndd  13280  grpinvcnv  13400  dfgrp3mlem  13430  prdsgrpd  13441  prdsinvgd  13442  eqglact  13561  ghmgrp2  13582  ghmlin  13584  ghmnsgpreima  13605  kerf1ghm  13610  srgdilem  13731  srgdir  13737  srgridm  13742  ringdilem  13774  ringdir  13781  ringridm  13786  unitmulcl  13875  unitnegcl  13892  rhmmhm  13921  elrhmunit  13939  lringuplu  13958  subrgring  13986  subrg1cl  13991  qusrhm  14290  znunit  14421  znrrg  14422  psrelbas  14437  mplsubgfilemcl  14461  mplsubgfileminv  14462  inopn  14475  restbasg  14640  ssrest  14654  cntop2  14674  icnpimaex  14683  cnima  14692  lmfss  14716  lmtopcnp  14722  txhmeo  14791  txswaphmeo  14793  psmet0  14799  psmettri2  14800  blhalf  14880  bdxmet  14973  xmetxpbl  14980  ioo2bl  15023  tgioo  15026  cncfi  15050  rescncf  15053  cdivcncfap  15076  cnopnap  15083  divcncfap  15086  dedekindeulemeu  15094  dedekindicclemeu  15103  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthinclemdisj  15112  ivthdec  15116  ivthreinc  15117  limcimo  15137  cnplimcim  15139  cnplimclemr  15141  cnlimci  15145  limccnpcntop  15147  limccnp2lem  15148  limccnp2cntop  15149  limccoap  15150  reldvg  15151  dvbsssg  15158  dvfgg  15160  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvrecap  15185  plyco  15231  plycj  15233  plyrecj  15235  sin0pilem1  15253  sin0pilem2  15254  tanrpcl  15309  tangtx  15310  cos0pilt1  15324  logbgcd1irraplemexp  15440  mpodvdsmulf1o  15462  perfect  15473  lgsne0  15515  lgseisen  15551  lgsquad2lem2  15559  2sqlem8a  15599  2sqlem8  15600  structgrssiedg  15640  bj-charfunbi  15747  bj-inf2vnlem1  15906  pwf1oexmid  15936  subctctexmid  15937  iooref1o  15973  taupi  16012  alsi2d  16021  alsc2d  16023