Theorem adantlrr 715

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 454	. 2 |- ( ( ps /\ ta ) -> ps )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl2 646	1 |- ( ( ( ph /\ ( ps /\ ta ) ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  oelim  6970  odi  7014  marypha1lem  7679  dfac12lem2  8309  infunsdom  8379  isf34lem4  8542  distrlem1pr  9190  drsdirfi  15104  isacs3lem  15332  conjnmzb  15774  psgndif  17991  frlmsslsp  18182  frlmsslspOLD  18183  metss2lem  20045  nghmcn  20283  bndth  20489  itg2monolem1  21187  dvmptfsum  21406  ply1divex  21567  itgulm  21832  rpvmasumlem  22695  dchrmusum2  22702  dchrisum0lem2  22726  dchrisum0lem3  22727  mulog2sumlem2  22743  pntibndlem3  22800  3v3e3cycl1  23465  4cycl4v4e  23487  blocni  24140  superpos  25693  chirredlem2  25730  eulerpartlemgvv  26689  ballotlemfc0  26805  ballotlemfcc  26806  fin2solem  28340  heicant  28351  ftc1anclem6  28397  ftc1anc  28400  fdc  28566  incsequz  28569  ismtyres  28632  isdrngo2  28689  rngohomco  28705  keridl  28757  mzpcompact2lem  29013  pellex  29101  monotuz  29207  unxpwdom3  29373  stoweidlem34  29754  bj-finsumval0  32308  linepsubN  33118  pmapsub  33134