Theorem adantlrl 756

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
adantlrl	|- ( ( ( ph /\ ( ta /\ ps ) ) /\ ch ) -> th )

Proof of Theorem adantlrl

Step	Hyp	Ref	Expression
1		simpr 477	. 2 |- ( ( ta /\ ps ) -> ps )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl2 683	1 |- ( ( ( ph /\ ( ta /\ ps ) ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  omlimcl  7658  odi  7659  oelim2  7675  mapxpen  8126  unwdomg  8489  dfac12lem2  8966  infunsdom  9036  fin1a2s  9236  frlmup1  20137  fbasrn  21688  lmmbr  23056  grporcan  27372  unoplin  28779  hmoplin  28801  superpos  29213  subfacp1lem5  31166  matunitlindflem1  33405  poimirlem4  33413  itg2addnclem  33461  ftc1anclem6  33490  fdc  33541  ismtyres  33607  isdrngo2  33757  rngohomco  33773  rngoisocnv  33780  dssmapnvod  38314  climxrrelem  39981  dvdsn1add  40154  dvnprodlem1  40161  stoweidlem27  40244  fourierdlem97  40420  qndenserrnbllem  40514  sge0iunmptlemfi  40630