Theorem adantlrr 726

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

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

Assertion

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

Proof of Theorem adantlrr

Step	Hyp	Ref	Expression
1		simpl 459	. 2 |- ( ( ps /\ ta ) -> ps )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl2 656	1 |- ( ( ( ph /\ ( ps /\ ta ) ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 189  df-an 373

This theorem is referenced by:  oelim  7233  odi  7277  marypha1lem  7944  dfac12lem2  8571  infunsdom  8641  isf34lem4  8804  distrlem1pr  9447  lcmgcdlem  14564  lcmdvds  14566  drsdirfi  16176  isacs3lem  16405  conjnmzb  16910  psgndif  19163  frlmsslsp  19347  metss2lem  21519  nghmcn  21759  bndth  21979  itg2monolem1  22701  dvmptfsum  22920  ply1divex  23080  itgulm  23356  rpvmasumlem  24318  dchrmusum2  24325  dchrisum0lem2  24349  dchrisum0lem3  24350  mulog2sumlem2  24366  pntibndlem3  24423  3v3e3cycl1  25365  4cycl4v4e  25387  blocni  26439  superpos  28000  chirredlem2  28037  eulerpartlemgvv  29202  ballotlemfc0  29318  ballotlemfcc  29319  bj-finsumval0  31695  fin2solem  31924  poimirlem28  31961  heicant  31968  ftc1anclem6  32015  ftc1anc  32018  fdc  32067  incsequz  32070  ismtyres  32133  isdrngo2  32190  rngohomco  32206  keridl  32258  linepsubN  33311  pmapsub  33327  mzpcompact2lem  35587  pellex  35673  monotuz  35783  unxpwdom3  35947  radcnvrat  36657  fprodexp  37668  fprodabs2  37669  dvnprodlem1  37815  stoweidlem34  37889  fourierdlem42  38006  fourierdlem42OLD  38007  elaa2  38093  sge0iunmptlemfi  38249  aacllem  40527