Theorem adantlr 462

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
adantlr	|- ( ( ( ph /\ th ) /\ ps ) -> ch )

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ph /\ th ) -> ph )
2		adant2.1	. 2 |- ( ( ph /\ ps ) -> ch )
3	1, 2	sylan 278	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad2antrr  473  ad2ant2r  494  ad2ant2rl  496  3ad2antl1  1108  3ad2antl2  1109  ad4ant124  1159  3adant1r  1174  bilukdc  1339  intab  3739  pofun  4163  ralxfrd  4312  rexxfrd  4313  ordtri2or2exmidlem  4370  wessep  4421  poinxp  4536  relop  4617  fun11iun  5309  ssimaex  5400  fndmdif  5443  fconst2g  5551  foeqcnvco  5607  f1eqcocnv  5608  isocnv  5628  isocnv2  5629  riota2df  5666  grprinvd  5878  grpridd  5879  f1o2ndf1  6031  tfr1onlembacc  6145  tfr1onlemaccex  6151  tfr1onlemres  6152  tfrcllembacc  6158  tfrcllemaccex  6164  tfrcllemres  6165  tfrcldm  6166  tfrcl  6167  xpdom2  6627  fimax2gtrilemstep  6696  xpfi  6720  eqsupti  6771  ordiso2  6808  enumctlemm  6872  mulcanpig  6991  prarloclemlt  7149  genpdf  7164  genpdisj  7179  addnqprl  7185  addnqpru  7186  addlocpr  7192  prmuloc  7222  mulnqprl  7224  mulnqpru  7225  mullocpr  7227  ltpopr  7251  ltsopr  7252  ltaddpr  7253  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemru  7268  addcanprleml  7270  addcanprlemu  7271  ltaprg  7275  recexprlemopu  7283  recexprlemloc  7287  cauappcvgprlemladdfl  7311  cauappcvgprlemladdru  7312  caucvgsrlemcau  7435  caucvgsrlemgt1  7437  caucvgsrlemoffcau  7440  caucvgsrlemoffres  7442  axcaucvglemcau  7530  cnegexlem1  7754  cnegexlem3  7756  cnegex  7757  addsubeq4  7794  rimul  8159  divcanap6  8283  ltmul12a  8418  lemul12b  8419  lbinf  8506  zrevaddcl  8898  nzadd  8900  zextle  8936  fzind  8960  uz11  9140  qreccl  9226  qrevaddcl  9228  irradd  9230  xrlttr  9364  xrltso  9365  xaddass  9435  xleadd1a  9439  xlt2add  9446  iccshftr  9560  iccshftl  9562  iccdil  9564  icccntr  9566  divelunit  9568  uzsubsubfz  9610  fzaddel  9622  fzrev  9647  elfzmlbp  9692  frec2uzrdg  9965  frecuzrdgtcl  9968  frecuzrdgsuc  9970  frecuzrdgdomlem  9973  frecuzrdgfunlem  9975  frecuzrdgsuctlem  9979  iseqovex  10016  iseqval  10017  iseqvalt  10019  seq3val  10020  iseqfclt  10025  seqf  10026  iseqsst  10031  seq3clss  10032  seq3fveq2  10034  seq3feq2  10035  seq3feq  10037  seq3shft2  10038  ser3mono  10044  seq3split  10045  seq3caopr3  10047  seq3caopr2  10048  iseqf1olemab  10055  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3f1olemqsum  10066  seq3f1olemstep  10067  seq3f1oleml  10069  seq3id3  10073  seq3id  10074  seq3id2  10075  seq3homo  10076  seq3z  10077  seqfeq3  10078  ser3ge0  10083  expp1  10093  expnegap0  10094  expcllem  10097  mulexp  10125  expadd  10128  expaddzap  10130  expmulzap  10132  expdivap  10137  leexp1a  10141  expnlbnd  10209  bcpasc  10305  bccl  10306  hashfacen  10372  seq3coll  10378  seq3shft  10403  resqrexlemfp1  10573  sqrtdiv  10606  climshftlemg  10861  climcn1  10867  climsqz  10893  climsqz2  10894  clim2ser  10895  clim2ser2  10896  isermulc2  10898  climub  10902  serf0  10910  fsum3cvg  10935  sumrbdc  10936  summodclem3  10938  summodclem2a  10939  zsumdc  10942  fsumf1o  10948  isumss  10949  fisumss  10950  isumss2  10951  fsum3cvg2  10952  fsum3cvg3  10954  fsumcl2lem  10956  fsumcllem  10957  fsumadd  10964  fsumsplit  10965  fsumsplitsn  10968  sumsplitdc  10990  fisumrev2  11004  fsum2mul  11011  fsum00  11020  telfsumo  11024  fsumparts  11028  iserabs  11033  cvgratnnlemabsle  11085  cvgratnn  11089  cvgratz  11090  mertenslemub  11092  mertenslemi1  11093  mertenslem2  11094  mertensabs  11095  eftlcvg  11141  negdvdsb  11254  dvdsnegb  11255  dvdsext  11298  addmodlteqALT  11302  nno  11348  infssuzex  11387  gcdsupex  11391  gcdsupcl  11392  bezoutlembz  11435  dvdssq  11462  eucalgf  11479  dvdslcm  11493  lcmledvds  11494  lcmeq0  11495  lcmcl  11496  lcmdvds  11503  lcmgcdeq  11507  divgcdcoprmex  11526  phibndlem  11634  phiprmpw  11640  opnssneib  12023  neissex  12032  tgrest  12036  iscnp3  12069  cnpnei  12085  cnrest  12101  elbl3ps  12195  elbl3  12196  blininf  12225  blssexps  12230  blssex  12231  blpnfctr  12240  mopni2  12284  blsscls2  12294  metss  12295  bdmet  12303  metrest  12307  metcn  12311  bl2ioo  12331