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  983  simp3  984  sbh  1753  eldifbd  3110  unssbd  3281  opth  4192  potr  4263  frind  4307  brrelex2  4620  funinsn  5212  feu  5345  fcnvres  5346  fun11iun  5428  elmpocl2  6010  oprssdmm  6109  tfrlem1  6245  tfrlemisucfn  6261  tfrlemisucaccv  6262  tfrlemibxssdm  6264  tfrlemibfn  6265  tfrlemi14d  6270  swoer  6497  elmapssres  6607  mapsspm  6616  pmsspw  6617  mapss  6625  dom0  6772  xpf1o  6778  sbthlemi8  6897  sbthlemi9  6898  supelti  6934  supisoti  6942  djulclb  6985  cardcl  7095  isnumi  7096  cardval3ex  7099  exmidonfinlem  7107  en2eleq  7109  acfun  7121  exmidaclem  7122  ccfunen  7163  indpi  7241  dfplpq2  7253  ltbtwnnq  7315  enq0tr  7333  nqnq0pi  7337  elnp1st2nd  7375  prcunqu  7384  prnmaxl  7387  prloc  7390  genpcuu  7419  addnqprllem  7426  addlocprlemeq  7432  addlocprlemgt  7433  addlocpr  7435  nqprxx  7445  gtnqex  7449  appdivnq  7462  prmuloclemcalc  7464  prmuloc  7465  mullocprlem  7469  ltprordil  7488  ltnqpri  7493  ltexprlemm  7499  ltexprlemopl  7500  ltexprlemlol  7501  ltexprlemopu  7502  ltexprlemupu  7503  ltexprlemdisj  7505  ltexprlemloc  7506  ltexprlemfl  7508  ltexprlemrl  7509  ltexprlemfu  7510  ltexprlemru  7511  ltexpri  7512  recexprlemell  7521  recexprlemelu  7522  recexprlemloc  7530  recexprlempr  7531  recexprlem1ssl  7532  recexprlem1ssu  7533  recexprlemss1l  7534  aptipr  7540  cauappcvgprlemlol  7546  cauappcvgprlemupu  7548  cauappcvgprlemladdfu  7553  cauappcvgprlemladdfl  7554  cauappcvgprlemladdrl  7556  caucvgprlemnkj  7565  caucvgprlemnbj  7566  caucvgprlemlol  7569  caucvgprlemupu  7571  caucvgprlemladdfu  7576  caucvgprlem1  7578  caucvgprlem2  7579  caucvgprprlemnjltk  7590  caucvgprprlemnbj  7592  caucvgprprlemlol  7597  caucvgprprlemupu  7599  caucvgprprlemexbt  7605  caucvgprprlem1  7608  caucvgprprlem2  7609  suplocexprlemrl  7616  suplocexprlemru  7618  suplocexprlemdisj  7619  suplocexprlemub  7622  suplocexprlemlub  7623  ltsrprg  7646  gt0srpr  7647  recexgt0sr  7672  addgt0sr  7674  mulgt0sr  7677  map2psrprg  7704  suplocsrlemb  7705  suplocsrlem  7707  nnindnn  7792  axcaucvglemcau  7797  axpre-suploclemres  7800  apreap  8441  apreim  8457  mulge0  8473  apti  8476  mulap0bbd  8513  lble  8797  nnind  8828  recnz  9236  uzind  9254  eluzadd  9446  eluzsub  9447  ixxss1  9786  ixxss2  9787  ixxss12  9788  iccss2  9826  iccssioo2  9828  iccssico2  9829  elfzolt2  10033  ioom  10138  elicore  10144  flqltp1  10156  addmodlteq  10275  expcl2lemap  10409  expap0i  10429  hashennnuni  10630  crre  10734  caucvgre  10858  cvg1nlemcau  10861  cvg1nlemres  10862  resqrexlemoverl  10898  sqrtge0  10910  fimaxre2  11103  climi  11161  reccn2ap  11187  climge0  11199  nnf1o  11250  sumpr  11287  fsump1i  11307  fsum00  11336  fsumparts  11344  mertenslemi1  11409  addsin  11616  subsin  11617  addcos  11620  subcos  11621  sinbnd2  11628  cosbnd2  11629  evenelz  11731  4dvdseven  11781  infssuzcldc  11811  gcd0id  11835  gcd1  11843  bezoutlemstep  11853  dvdsgcdb  11869  mulgcd  11872  gcdzeq  11878  dvdsmulgcd  11881  sqgcd  11885  dvdssqlem  11886  bezoutr  11888  lcmval  11912  lcmcllem  11916  lcmgcdlem  11926  lcmdvds  11928  lcmgcdeq  11932  lcmdvdsb  11933  mulgcddvds  11943  rpmulgcd2  11944  qredeu  11946  rpdvds  11948  divgcdcoprm0  11950  isprm3  11967  divgcdodd  11989  coprm  11990  rpexp  11999  sqrt2irr  12008  qdencl  12035  qeqnumdivden  12040  divnumden  12042  divdenle  12043  densq  12050  phimullem  12069  eulerthlem1  12071  eulerthlemrprm  12073  eulerthlemth  12076  hashgcdeq  12079  ennnfonelemom  12096  ennnfonelemex  12102  ennnfonelemf1  12106  ctiunctlemu1st  12122  ctiunctlemu2nd  12123  inopn  12348  restbasg  12515  ssrest  12529  cntop2  12549  icnpimaex  12558  cnima  12567  lmfss  12591  lmtopcnp  12597  txhmeo  12666  txswaphmeo  12668  psmet0  12674  psmettri2  12675  blhalf  12755  bdxmet  12848  xmetxpbl  12855  ioo2bl  12890  tgioo  12893  cncfi  12912  rescncf  12915  cdivcncfap  12934  cnopnap  12941  dedekindeulemeu  12947  dedekindicclemeu  12956  ivthinclemum  12960  ivthinclemlopn  12961  ivthinclemuopn  12963  ivthinclemdisj  12965  ivthdec  12969  limcimo  12981  cnplimcim  12983  cnplimclemr  12985  cnlimci  12989  limccnpcntop  12991  limccnp2lem  12992  limccnp2cntop  12993  limccoap  12994  reldvg  12995  dvbsssg  13002  dvfgg  13004  dvaddxxbr  13012  dvmulxxbr  13013  dvcoapbr  13018  dvcjbr  13019  dvrecap  13024  sin0pilem1  13049  sin0pilem2  13050  tanrpcl  13105  tangtx  13106  cos0pilt1  13120  logbgcd1irraplemexp  13232  bj-charfunbi  13332  bj-inf2vnlem1  13491  pwf1oexmid  13518  subctctexmid  13520  iooref1o  13554  taupi  13590  alsi2d  13599  alsc2d  13601