Theorem adantlrr 702

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  tfrlem2  6596  oelim  6737  odi  6781  marypha1lem  7396  dfac12lem2  7980  infunsdom  8050  isf34lem4  8213  distrlem1pr  8858  drsdirfi  14350  isacs3lem  14547  conjnmzb  14995  metss2lem  18494  nghmcn  18732  bndth  18936  itg2monolem1  19595  dvmptfsum  19812  ply1divex  20012  itgulm  20277  rpvmasumlem  21134  dchrmusum2  21141  dchrisum0lem2  21165  dchrisum0lem3  21166  mulog2sumlem2  21182  pntibndlem3  21239  3v3e3cycl1  21584  4cycl4v4e  21606  blocni  22259  superpos  23810  chirredlem2  23847  ballotlemfc0  24703  ballotlemfcc  24704  fdc  26339  incsequz  26342  ismtyres  26407  isdrngo2  26464  rngohomco  26480  keridl  26532  mzpcompact2lem  26698  pellex  26788  monotuz  26894  frlmsslsp  27116  stoweidlem34  27650  linepsubN  30234  pmapsub  30250

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

This theorem depends on definitions:  df-bi 178  df-an 361