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  4288  potr  4362  frind  4406  brrelex2  4723  funinsn  5331  feu  5469  fcnvres  5470  fun11iun  5554  funopsn  5774  elmpocl2  6155  uchoice  6235  oprssdmm  6269  tfrlem1  6406  tfrlemisucfn  6422  tfrlemisucaccv  6423  tfrlemibxssdm  6425  tfrlemibfn  6426  tfrlemi14d  6431  swoer  6660  elmapssres  6772  mapsspm  6781  pmsspw  6782  mapss  6790  dom0  6949  xpf1o  6955  sbthlemi8  7080  sbthlemi9  7081  supelti  7118  supisoti  7126  djulclb  7171  nninfninc  7239  nnnninfeq2  7245  cardcl  7302  isnumi  7303  cardval3ex  7306  exmidonfinlem  7316  en2eleq  7318  finacn  7331  acfun  7334  exmidaclem  7335  dftap2  7378  exmidapne  7387  ccfunen  7391  acnccim  7399  indpi  7470  dfplpq2  7482  ltbtwnnq  7544  enq0tr  7562  nqnq0pi  7566  elnp1st2nd  7604  prcunqu  7613  prnmaxl  7616  prloc  7619  genpcuu  7648  addnqprllem  7655  addlocprlemeq  7661  addlocprlemgt  7662  addlocpr  7664  nqprxx  7674  gtnqex  7678  appdivnq  7691  prmuloclemcalc  7693  prmuloc  7694  mullocprlem  7698  ltprordil  7717  ltnqpri  7722  ltexprlemm  7728  ltexprlemopl  7729  ltexprlemlol  7730  ltexprlemopu  7731  ltexprlemupu  7732  ltexprlemdisj  7734  ltexprlemloc  7735  ltexprlemfl  7737  ltexprlemrl  7738  ltexprlemfu  7739  ltexprlemru  7740  ltexpri  7741  recexprlemell  7750  recexprlemelu  7751  recexprlemloc  7759  recexprlempr  7760  recexprlem1ssl  7761  recexprlem1ssu  7762  recexprlemss1l  7763  aptipr  7769  cauappcvgprlemlol  7775  cauappcvgprlemupu  7777  cauappcvgprlemladdfu  7782  cauappcvgprlemladdfl  7783  cauappcvgprlemladdrl  7785  caucvgprlemnkj  7794  caucvgprlemnbj  7795  caucvgprlemlol  7798  caucvgprlemupu  7800  caucvgprlemladdfu  7805  caucvgprlem1  7807  caucvgprlem2  7808  caucvgprprlemnjltk  7819  caucvgprprlemnbj  7821  caucvgprprlemlol  7826  caucvgprprlemupu  7828  caucvgprprlemexbt  7834  caucvgprprlem1  7837  caucvgprprlem2  7838  suplocexprlemrl  7845  suplocexprlemru  7847  suplocexprlemdisj  7848  suplocexprlemub  7851  suplocexprlemlub  7852  ltsrprg  7875  gt0srpr  7876  recexgt0sr  7901  addgt0sr  7903  mulgt0sr  7906  map2psrprg  7933  suplocsrlemb  7934  suplocsrlem  7936  nnindnn  8021  axcaucvglemcau  8026  axpre-suploclemres  8029  apreap  8675  apreim  8691  mulge0  8707  apti  8710  mulap0bbd  8748  lble  9035  nnind  9067  recnz  9481  uzind  9499  eluzadd  9692  eluzsub  9693  ixxss1  10041  ixxss2  10042  ixxss12  10043  iccss2  10081  iccssioo2  10083  iccssico2  10084  elfzolt2  10294  infssuzcldc  10395  ioom  10420  elicore  10426  flqltp1  10439  addmodlteq  10560  expcl2lemap  10713  expap0i  10733  hashennnuni  10941  hashdmprop2dom  11006  wrdexb  11023  swrdsbslen  11137  swrdspsleq  11138  crre  11238  caucvgre  11362  cvg1nlemcau  11365  cvg1nlemres  11366  resqrexlemoverl  11402  sqrtge0  11414  fimaxre2  11608  climi  11668  reccn2ap  11694  climge0  11706  nnf1o  11757  sumpr  11794  fsump1i  11814  fsum00  11843  fsumparts  11851  mertenslemi1  11916  addsin  12123  subsin  12124  addcos  12127  subcos  12128  sinbnd2  12135  cosbnd2  12136  sinltxirr  12142  dvdsaddre2b  12222  evenelz  12248  4dvdseven  12298  gcd0id  12370  gcd1  12378  bezoutlemstep  12388  dvdsgcdb  12404  mulgcd  12407  gcdzeq  12413  dvdsmulgcd  12416  sqgcd  12420  dvdssqlem  12421  bezoutr  12423  uzwodc  12428  nninfctlemfo  12431  lcmval  12455  lcmcllem  12459  lcmgcdlem  12469  lcmdvds  12471  lcmgcdeq  12475  lcmdvdsb  12476  mulgcddvds  12486  rpmulgcd2  12487  qredeu  12489  rpdvds  12491  divgcdcoprm0  12493  isprm3  12510  divgcdodd  12535  coprm  12536  rpexp  12545  sqrt2irr  12554  qdencl  12581  qeqnumdivden  12586  divnumden  12588  divdenle  12589  densq  12596  phimullem  12617  eulerthlem1  12619  eulerthlemrprm  12621  eulerthlemth  12624  prmdiveq  12628  prmdivdiv  12629  hashgcdeq  12632  phisum  12633  odzid  12637  reumodprminv  12646  oddn2prm  12654  pythagtriplem4  12661  pythagtriplem11  12667  pythagtriplem13  12669  pythagtriplem19  12675  pclemub  12680  pcprendvds2  12684  pcpre1  12685  pcpremul  12686  pceulem  12687  pczdvds  12707  pc2dvds  12723  pcaddlem  12732  pcmpt  12736  pcmpt2  12737  pcmptdvds  12738  pcprod  12739  pockthlem  12749  pockthg  12750  prmunb  12755  1arithlem4  12759  4sqlem7  12777  4sqlem8  12778  4sqlem9  12779  4sqlem10  12780  4sqlemffi  12789  4sqlem15  12798  4sqlem16  12799  4sqlem17  12800  4sqlem18  12801  ennnfonelemom  12849  ennnfonelemex  12855  ennnfonelemf1  12859  ctiunctlemu1st  12875  ctiunctlemu2nd  12876  fnpr2ob  13242  mgmlrid  13281  gsumfzval  13293  gsumval2  13299  mndrid  13338  prdsmndd  13350  grpinvcnv  13470  dfgrp3mlem  13500  prdsgrpd  13511  prdsinvgd  13512  eqglact  13631  ghmgrp2  13652  ghmlin  13654  ghmnsgpreima  13675  kerf1ghm  13680  srgdilem  13801  srgdir  13807  srgridm  13812  ringdilem  13844  ringdir  13851  ringridm  13856  unitmulcl  13945  unitnegcl  13962  rhmmhm  13991  elrhmunit  14009  lringuplu  14028  subrgring  14056  subrg1cl  14061  qusrhm  14360  znunit  14491  znrrg  14492  psrelbas  14507  mplsubgfilemcl  14531  mplsubgfileminv  14532  inopn  14545  restbasg  14710  ssrest  14724  cntop2  14744  icnpimaex  14753  cnima  14762  lmfss  14786  lmtopcnp  14792  txhmeo  14861  txswaphmeo  14863  psmet0  14869  psmettri2  14870  blhalf  14950  bdxmet  15043  xmetxpbl  15050  ioo2bl  15093  tgioo  15096  cncfi  15120  rescncf  15123  cdivcncfap  15146  cnopnap  15153  divcncfap  15156  dedekindeulemeu  15164  dedekindicclemeu  15173  ivthinclemum  15177  ivthinclemlopn  15178  ivthinclemuopn  15180  ivthinclemdisj  15182  ivthdec  15186  ivthreinc  15187  limcimo  15207  cnplimcim  15209  cnplimclemr  15211  cnlimci  15215  limccnpcntop  15217  limccnp2lem  15218  limccnp2cntop  15219  limccoap  15220  reldvg  15221  dvbsssg  15228  dvfgg  15230  dvaddxxbr  15243  dvmulxxbr  15244  dvcoapbr  15249  dvcjbr  15250  dvrecap  15255  plyco  15301  plycj  15303  plyrecj  15305  sin0pilem1  15323  sin0pilem2  15324  tanrpcl  15379  tangtx  15380  cos0pilt1  15394  logbgcd1irraplemexp  15510  mpodvdsmulf1o  15532  perfect  15543  lgsne0  15585  lgseisen  15621  lgsquad2lem2  15629  2sqlem8a  15669  2sqlem8  15670  structgrssiedg  15712  uhgrm  15744  bj-charfunbi  15881  bj-inf2vnlem1  16040  pwf1oexmid  16071  subctctexmid  16072  iooref1o  16108  taupi  16147  alsi2d  16156  alsc2d  16158