Theorem adantlrr 719

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

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  oelim  7221  odi  7265  marypha1lem  7927  dfac12lem2  8556  infunsdom  8626  isf34lem4  8789  distrlem1pr  9433  drsdirfi  15891  isacs3lem  16120  conjnmzb  16625  psgndif  18936  frlmsslsp  19123  metss2lem  21306  nghmcn  21544  bndth  21750  itg2monolem1  22449  dvmptfsum  22668  ply1divex  22829  itgulm  23095  rpvmasumlem  24053  dchrmusum2  24060  dchrisum0lem2  24084  dchrisum0lem3  24085  mulog2sumlem2  24101  pntibndlem3  24158  3v3e3cycl1  25061  4cycl4v4e  25083  blocni  26134  superpos  27686  chirredlem2  27723  eulerpartlemgvv  28821  ballotlemfc0  28937  ballotlemfcc  28938  bj-finsumval0  31227  fin2solem  31411  heicant  31421  ftc1anclem6  31468  ftc1anc  31471  fdc  31520  incsequz  31523  ismtyres  31586  isdrngo2  31643  rngohomco  31659  keridl  31711  linepsubN  32769  pmapsub  32785  mzpcompact2lem  35045  pellex  35132  monotuz  35238  unxpwdom3  35403  radcnvrat  36043  lcmgcdlem  36060  lcmdvds  36062  fprodexp  36968  fprodabs2  36970  dvnprodlem1  37111  stoweidlem34  37184  fourierdlem42  37299  elaa2  37385  aacllem  38860