Theorem adantlr 469

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 281	1 |- ( ( ( ph /\ th ) /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad2antrr  480  ad2ant2r  501  ad2ant2rl  503  adantl3r  504  ad4ant14  506  ad4ant24  508  ad5ant13  511  ad5ant14  512  ad5ant15  513  3ad2antl1  1149  3ad2antl2  1150  ad4ant124  1206  3adant1r  1221  bilukdc  1386  intab  3852  pofun  4289  ralxfrd  4439  rexxfrd  4440  ordtri2or2exmidlem  4502  wessep  4554  poinxp  4672  relop  4753  fun11iun  5452  ssimaex  5546  fndmdif  5589  fconst2g  5699  foeqcnvco  5757  f1eqcocnv  5758  isocnv  5778  isocnv2  5779  riota2df  5817  grprinvd  6033  grpridd  6034  f1o2ndf1  6192  tfr1onlembacc  6306  tfr1onlemaccex  6312  tfr1onlemres  6313  tfrcllembacc  6319  tfrcllemaccex  6325  tfrcllemres  6326  tfrcldm  6327  tfrcl  6328  xpdom2  6793  fimax2gtrilemstep  6862  xpfi  6891  eqsupti  6957  ordiso2  6996  enumctlemm  7075  enwomnilem  7129  cc2lem  7203  mulcanpig  7272  prarloclemlt  7430  genpdf  7445  genpdisj  7460  addnqprl  7466  addnqpru  7467  addlocpr  7473  prmuloc  7503  mulnqprl  7505  mulnqpru  7506  mullocpr  7508  ltpopr  7532  ltsopr  7533  ltaddpr  7534  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  ltaprg  7556  recexprlemopu  7564  recexprlemloc  7568  cauappcvgprlemladdfl  7592  cauappcvgprlemladdru  7593  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffcau  7735  caucvgsrlemoffres  7737  suplocsrlem  7745  axcaucvglemcau  7835  axpre-suploclemres  7838  axsuploc  7967  cnegexlem1  8069  cnegexlem3  8071  cnegex  8072  addsubeq4  8109  rimul  8479  divcanap6  8611  ltmul12a  8751  lemul12b  8752  lbinf  8839  zrevaddcl  9237  nzadd  9239  zextle  9278  fzind  9302  uz11  9484  infregelbex  9532  qreccl  9576  qrevaddcl  9578  irradd  9580  xrlttr  9727  xrltso  9728  xaddass  9801  xleadd1a  9805  xlt2add  9812  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  divelunit  9934  uzsubsubfz  9978  fzaddel  9990  fzrev  10015  elfzmlbp  10063  frec2uzrdg  10340  frecuzrdgtcl  10343  frecuzrdgsuc  10345  frecuzrdgdomlem  10348  frecuzrdgfunlem  10350  frecuzrdgsuctlem  10354  iseqovex  10387  seq3val  10389  seqf  10392  seq3clss  10398  seq3fveq2  10400  seq3feq2  10401  seq3feq  10403  seq3shft2  10404  ser3mono  10409  seq3split  10410  seq3caopr3  10412  seq3caopr2  10413  iseqf1olemab  10420  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemstep  10432  seq3f1oleml  10434  seq3id3  10438  seq3id  10439  seq3id2  10440  seq3homo  10441  seq3z  10442  seqfeq3  10443  ser3ge0  10448  expp1  10458  expnegap0  10459  expcllem  10462  mulexp  10490  expadd  10493  expaddzap  10495  expmulzap  10497  expdivap  10502  leexp1a  10506  expnlbnd  10575  bcpasc  10675  bccl  10676  hashfacen  10745  seq3coll  10751  seq3shft  10776  resqrexlemfp1  10947  sqrtdiv  10980  climshftlemg  11239  climcn1  11245  climsqz  11272  climsqz2  11273  clim2ser  11274  clim2ser2  11275  isermulc2  11277  climub  11281  serf0  11289  fsum3cvg  11315  sumrbdc  11316  summodclem3  11317  summodclem2a  11318  zsumdc  11321  fsumf1o  11327  isumss  11328  fisumss  11329  isumss2  11330  fsum3cvg2  11331  fsum3cvg3  11333  fsumcl2lem  11335  fsumcllem  11336  fsumadd  11343  fsumsplit  11344  fsumsplitsn  11347  sumsplitdc  11369  fisumrev2  11383  fsum2mul  11390  fsum00  11399  telfsumo  11403  fsumparts  11407  iserabs  11412  cvgratnnlemabsle  11464  cvgratnn  11468  cvgratz  11469  mertenslemub  11471  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  clim2prod  11476  clim2divap  11477  prodfap0  11482  prodfrecap  11483  prodeq2  11494  fproddccvg  11509  prodrbdclem2  11510  prodmodc  11515  zproddc  11516  fprodf1o  11525  fprodssdc  11527  fprodunsn  11541  fprodcllem  11543  fprodabs  11553  fprodeq0  11554  fprodmodd  11578  eftlcvg  11624  negdvdsb  11743  dvdsnegb  11744  dvdsext  11789  addmodlteqALT  11793  nno  11839  infssuzex  11878  zsupssdc  11883  gcdsupex  11886  gcdsupcl  11887  bezoutlembz  11933  dvdssq  11960  eucalgf  11983  dvdslcm  11997  lcmledvds  11998  lcmeq0  11999  lcmcl  12000  lcmdvds  12007  lcmgcdeq  12011  divgcdcoprmex  12030  isprm5lem  12069  phibndlem  12144  phiprmpw  12150  pc2dvds  12257  pcmpt  12269  prmpwdvds  12281  1arith  12293  ctiunctlemf  12367  ctiunct  12369  opnssneib  12756  neissex  12765  tgrest  12769  iscnp3  12803  cnpnei  12819  cnrest  12835  tx1cn  12869  txcnp  12871  elbl3ps  12994  elbl3  12995  blininf  13024  blssexps  13029  blssex  13030  blpnfctr  13039  mopni2  13083  blsscls2  13093  metss  13094  bdmet  13102  metrest  13106  metcn  13114  txmetcn  13119  bl2ioo  13142  ivthinclemlr  13215  ivthinclemur  13217  dvcj  13273  dvfre  13274  coseq0q4123  13355  abssinper  13367  lgsval2lem  13511  lgsval4lem  13512  lgsneg  13525  lgsmod  13527  lgsdir2  13534  lgsdir  13536  lgsne0  13539  lgssq  13541  subctctexmid  13841  cvgcmp2n  13872  iswomninnlem  13888  nconstwlpo  13904