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  988  simp3  989  sbh  1764  eldifbd  3127  unssbd  3299  opth  4214  potr  4285  frind  4329  brrelex2  4644  funinsn  5236  feu  5369  fcnvres  5370  fun11iun  5452  elmpocl2  6037  oprssdmm  6136  tfrlem1  6272  tfrlemisucfn  6288  tfrlemisucaccv  6289  tfrlemibxssdm  6291  tfrlemibfn  6292  tfrlemi14d  6297  swoer  6525  elmapssres  6635  mapsspm  6644  pmsspw  6645  mapss  6653  dom0  6800  xpf1o  6806  sbthlemi8  6925  sbthlemi9  6926  supelti  6963  supisoti  6971  djulclb  7016  nnnninfeq2  7089  cardcl  7133  isnumi  7134  cardval3ex  7137  exmidonfinlem  7145  en2eleq  7147  acfun  7159  exmidaclem  7160  ccfunen  7201  indpi  7279  dfplpq2  7291  ltbtwnnq  7353  enq0tr  7371  nqnq0pi  7375  elnp1st2nd  7413  prcunqu  7422  prnmaxl  7425  prloc  7428  genpcuu  7457  addnqprllem  7464  addlocprlemeq  7470  addlocprlemgt  7471  addlocpr  7473  nqprxx  7483  gtnqex  7487  appdivnq  7500  prmuloclemcalc  7502  prmuloc  7503  mullocprlem  7507  ltprordil  7526  ltnqpri  7531  ltexprlemm  7537  ltexprlemopl  7538  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemfl  7546  ltexprlemrl  7547  ltexprlemfu  7548  ltexprlemru  7549  ltexpri  7550  recexprlemell  7559  recexprlemelu  7560  recexprlemloc  7568  recexprlempr  7569  recexprlem1ssl  7570  recexprlem1ssu  7571  recexprlemss1l  7572  aptipr  7578  cauappcvgprlemlol  7584  cauappcvgprlemupu  7586  cauappcvgprlemladdfu  7591  cauappcvgprlemladdfl  7592  cauappcvgprlemladdrl  7594  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemlol  7607  caucvgprlemupu  7609  caucvgprlemladdfu  7614  caucvgprlem1  7616  caucvgprlem2  7617  caucvgprprlemnjltk  7628  caucvgprprlemnbj  7630  caucvgprprlemlol  7635  caucvgprprlemupu  7637  caucvgprprlemexbt  7643  caucvgprprlem1  7646  caucvgprprlem2  7647  suplocexprlemrl  7654  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemub  7660  suplocexprlemlub  7661  ltsrprg  7684  gt0srpr  7685  recexgt0sr  7710  addgt0sr  7712  mulgt0sr  7715  map2psrprg  7742  suplocsrlemb  7743  suplocsrlem  7745  nnindnn  7830  axcaucvglemcau  7835  axpre-suploclemres  7838  apreap  8481  apreim  8497  mulge0  8513  apti  8516  mulap0bbd  8553  lble  8838  nnind  8869  recnz  9280  uzind  9298  eluzadd  9490  eluzsub  9491  ixxss1  9836  ixxss2  9837  ixxss12  9838  iccss2  9876  iccssioo2  9878  iccssico2  9879  elfzolt2  10087  ioom  10192  elicore  10198  flqltp1  10210  addmodlteq  10329  expcl2lemap  10463  expap0i  10483  hashennnuni  10688  crre  10795  caucvgre  10919  cvg1nlemcau  10922  cvg1nlemres  10923  resqrexlemoverl  10959  sqrtge0  10971  fimaxre2  11164  climi  11224  reccn2ap  11250  climge0  11262  nnf1o  11313  sumpr  11350  fsump1i  11370  fsum00  11399  fsumparts  11407  mertenslemi1  11472  addsin  11679  subsin  11680  addcos  11683  subcos  11684  sinbnd2  11691  cosbnd2  11692  evenelz  11800  4dvdseven  11850  infssuzcldc  11880  gcd0id  11908  gcd1  11916  bezoutlemstep  11926  dvdsgcdb  11942  mulgcd  11945  gcdzeq  11951  dvdsmulgcd  11954  sqgcd  11958  dvdssqlem  11959  bezoutr  11961  uzwodc  11966  lcmval  11991  lcmcllem  11995  lcmgcdlem  12005  lcmdvds  12007  lcmgcdeq  12011  lcmdvdsb  12012  mulgcddvds  12022  rpmulgcd2  12023  qredeu  12025  rpdvds  12027  divgcdcoprm0  12029  isprm3  12046  divgcdodd  12071  coprm  12072  rpexp  12081  sqrt2irr  12090  qdencl  12117  qeqnumdivden  12122  divnumden  12124  divdenle  12125  densq  12132  phimullem  12153  eulerthlem1  12155  eulerthlemrprm  12157  eulerthlemth  12160  prmdiveq  12164  prmdivdiv  12165  hashgcdeq  12167  phisum  12168  odzid  12172  reumodprminv  12181  oddn2prm  12189  pythagtriplem4  12196  pythagtriplem11  12202  pythagtriplem13  12204  pythagtriplem19  12210  pclemub  12215  pcprendvds2  12219  pcpre1  12220  pcpremul  12221  pceulem  12222  pczdvds  12241  pc2dvds  12257  pcaddlem  12266  pcmpt  12269  pcmpt2  12270  pcmptdvds  12271  pcprod  12272  pockthlem  12282  pockthg  12283  prmunb  12288  1arithlem4  12292  4sqlem7  12310  4sqlem8  12311  4sqlem9  12312  4sqlem10  12313  ennnfonelemom  12337  ennnfonelemex  12343  ennnfonelemf1  12347  ctiunctlemu1st  12363  ctiunctlemu2nd  12364  inopn  12601  restbasg  12768  ssrest  12782  cntop2  12802  icnpimaex  12811  cnima  12820  lmfss  12844  lmtopcnp  12850  txhmeo  12919  txswaphmeo  12921  psmet0  12927  psmettri2  12928  blhalf  13008  bdxmet  13101  xmetxpbl  13108  ioo2bl  13143  tgioo  13146  cncfi  13165  rescncf  13168  cdivcncfap  13187  cnopnap  13194  dedekindeulemeu  13200  dedekindicclemeu  13209  ivthinclemum  13213  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinclemdisj  13218  ivthdec  13222  limcimo  13234  cnplimcim  13236  cnplimclemr  13238  cnlimci  13242  limccnpcntop  13244  limccnp2lem  13245  limccnp2cntop  13246  limccoap  13247  reldvg  13248  dvbsssg  13255  dvfgg  13257  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  sin0pilem1  13302  sin0pilem2  13303  tanrpcl  13358  tangtx  13359  cos0pilt1  13373  logbgcd1irraplemexp  13486  lgsne0  13539  2sqlem8a  13558  2sqlem8  13559  bj-charfunbi  13653  bj-inf2vnlem1  13812  pwf1oexmid  13839  subctctexmid  13841  iooref1o  13873  taupi  13909  alsi2d  13918  alsc2d  13920