Theorem adantlrr 720

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 457	. 2 |- ( ( ps /\ ta ) -> ps )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl2 651	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  6989  odi  7033  marypha1lem  7698  dfac12lem2  8328  infunsdom  8398  isf34lem4  8561  distrlem1pr  9209  drsdirfi  15123  isacs3lem  15351  conjnmzb  15796  psgndif  18047  frlmsslsp  18238  frlmsslspOLD  18239  metss2lem  20101  nghmcn  20339  bndth  20545  itg2monolem1  21243  dvmptfsum  21462  ply1divex  21623  itgulm  21888  rpvmasumlem  22751  dchrmusum2  22758  dchrisum0lem2  22782  dchrisum0lem3  22783  mulog2sumlem2  22799  pntibndlem3  22856  3v3e3cycl1  23545  4cycl4v4e  23567  blocni  24220  superpos  25773  chirredlem2  25810  eulerpartlemgvv  26774  ballotlemfc0  26890  ballotlemfcc  26891  fin2solem  28434  heicant  28445  ftc1anclem6  28491  ftc1anc  28494  fdc  28660  incsequz  28663  ismtyres  28726  isdrngo2  28783  rngohomco  28799  keridl  28851  mzpcompact2lem  29107  pellex  29195  monotuz  29301  unxpwdom3  29467  stoweidlem34  29848  bj-finsumval0  32602  linepsubN  33415  pmapsub  33431