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  1144  3ad2antl2  1145  ad4ant124  1195  3adant1r  1210  bilukdc  1375  intab  3808  pofun  4242  ralxfrd  4391  rexxfrd  4392  ordtri2or2exmidlem  4449  wessep  4500  poinxp  4616  relop  4697  fun11iun  5396  ssimaex  5490  fndmdif  5533  fconst2g  5643  foeqcnvco  5699  f1eqcocnv  5700  isocnv  5720  isocnv2  5721  riota2df  5758  grprinvd  5974  grpridd  5975  f1o2ndf1  6133  tfr1onlembacc  6247  tfr1onlemaccex  6253  tfr1onlemres  6254  tfrcllembacc  6260  tfrcllemaccex  6266  tfrcllemres  6267  tfrcldm  6268  tfrcl  6269  xpdom2  6733  fimax2gtrilemstep  6802  xpfi  6826  eqsupti  6891  ordiso2  6928  enumctlemm  7007  enwomnilem  7050  cc2lem  7098  mulcanpig  7167  prarloclemlt  7325  genpdf  7340  genpdisj  7355  addnqprl  7361  addnqpru  7362  addlocpr  7368  prmuloc  7398  mulnqprl  7400  mulnqpru  7401  mullocpr  7403  ltpopr  7427  ltsopr  7428  ltaddpr  7429  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemru  7444  addcanprleml  7446  addcanprlemu  7447  ltaprg  7451  recexprlemopu  7459  recexprlemloc  7463  cauappcvgprlemladdfl  7487  cauappcvgprlemladdru  7488  caucvgsrlemcau  7625  caucvgsrlemgt1  7627  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  suplocsrlem  7640  axcaucvglemcau  7730  axpre-suploclemres  7733  axsuploc  7861  cnegexlem1  7961  cnegexlem3  7963  cnegex  7964  addsubeq4  8001  rimul  8371  divcanap6  8503  ltmul12a  8642  lemul12b  8643  lbinf  8730  zrevaddcl  9128  nzadd  9130  zextle  9166  fzind  9190  uz11  9372  qreccl  9461  qrevaddcl  9463  irradd  9465  xrlttr  9611  xrltso  9612  xaddass  9682  xleadd1a  9686  xlt2add  9693  iccshftr  9807  iccshftl  9809  iccdil  9811  icccntr  9813  divelunit  9815  uzsubsubfz  9858  fzaddel  9870  fzrev  9895  elfzmlbp  9940  frec2uzrdg  10213  frecuzrdgtcl  10216  frecuzrdgsuc  10218  frecuzrdgdomlem  10221  frecuzrdgfunlem  10223  frecuzrdgsuctlem  10227  iseqovex  10260  seq3val  10262  seqf  10265  seq3clss  10271  seq3fveq2  10273  seq3feq2  10274  seq3feq  10276  seq3shft2  10277  ser3mono  10282  seq3split  10283  seq3caopr3  10285  seq3caopr2  10286  iseqf1olemab  10293  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemstep  10305  seq3f1oleml  10307  seq3id3  10311  seq3id  10312  seq3id2  10313  seq3homo  10314  seq3z  10315  seqfeq3  10316  ser3ge0  10321  expp1  10331  expnegap0  10332  expcllem  10335  mulexp  10363  expadd  10366  expaddzap  10368  expmulzap  10370  expdivap  10375  leexp1a  10379  expnlbnd  10447  bcpasc  10544  bccl  10545  hashfacen  10611  seq3coll  10617  seq3shft  10642  resqrexlemfp1  10813  sqrtdiv  10846  climshftlemg  11103  climcn1  11109  climsqz  11136  climsqz2  11137  clim2ser  11138  clim2ser2  11139  isermulc2  11141  climub  11145  serf0  11153  fsum3cvg  11179  sumrbdc  11180  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumf1o  11191  isumss  11192  fisumss  11193  isumss2  11194  fsum3cvg2  11195  fsum3cvg3  11197  fsumcl2lem  11199  fsumcllem  11200  fsumadd  11207  fsumsplit  11208  fsumsplitsn  11211  sumsplitdc  11233  fisumrev2  11247  fsum2mul  11254  fsum00  11263  telfsumo  11267  fsumparts  11271  iserabs  11276  cvgratnnlemabsle  11328  cvgratnn  11332  cvgratz  11333  mertenslemub  11335  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  clim2prod  11340  clim2divap  11341  prodfap0  11346  prodfrecap  11347  prodeq2  11358  fproddccvg  11373  prodrbdclem2  11374  prodmodc  11379  zproddc  11380  eftlcvg  11430  negdvdsb  11545  dvdsnegb  11546  dvdsext  11589  addmodlteqALT  11593  nno  11639  infssuzex  11678  gcdsupex  11682  gcdsupcl  11683  bezoutlembz  11728  dvdssq  11755  eucalgf  11772  dvdslcm  11786  lcmledvds  11787  lcmeq0  11788  lcmcl  11789  lcmdvds  11796  lcmgcdeq  11800  divgcdcoprmex  11819  phibndlem  11928  phiprmpw  11934  ctiunctlemf  11987  ctiunct  11989  opnssneib  12364  neissex  12373  tgrest  12377  iscnp3  12411  cnpnei  12427  cnrest  12443  tx1cn  12477  txcnp  12479  elbl3ps  12602  elbl3  12603  blininf  12632  blssexps  12637  blssex  12638  blpnfctr  12647  mopni2  12691  blsscls2  12701  metss  12702  bdmet  12710  metrest  12714  metcn  12722  txmetcn  12727  bl2ioo  12750  ivthinclemlr  12823  ivthinclemur  12825  dvcj  12881  dvfre  12882  coseq0q4123  12963  abssinper  12975  subctctexmid  13369  cvgcmp2n  13403  iswomninnlem  13417