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  7181  odi  7225  marypha1lem  7889  dfac12lem2  8520  infunsdom  8590  isf34lem4  8753  distrlem1pr  9399  drsdirfi  15421  isacs3lem  15649  conjnmzb  16096  psgndif  18405  frlmsslsp  18596  frlmsslspOLD  18597  metss2lem  20749  nghmcn  20987  bndth  21193  itg2monolem1  21892  dvmptfsum  22111  ply1divex  22272  itgulm  22537  rpvmasumlem  23400  dchrmusum2  23407  dchrisum0lem2  23431  dchrisum0lem3  23432  mulog2sumlem2  23448  pntibndlem3  23505  3v3e3cycl1  24320  4cycl4v4e  24342  blocni  25396  superpos  26949  chirredlem2  26986  eulerpartlemgvv  27955  ballotlemfc0  28071  ballotlemfcc  28072  fin2solem  29616  heicant  29626  ftc1anclem6  29672  ftc1anc  29675  fdc  29841  incsequz  29844  ismtyres  29907  isdrngo2  29964  rngohomco  29980  keridl  30032  mzpcompact2lem  30288  pellex  30375  monotuz  30481  unxpwdom3  30645  lcmgcdlem  30812  lcmdvds  30814  stoweidlem34  31334  fourierdlem42  31449  bj-finsumval0  33735  linepsubN  34548  pmapsub  34564