Theorem adantlll 715

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
adantlll	|- ( ( ( ( ta /\ ph ) /\ ps ) /\ ch ) -> th )

Proof of Theorem adantlll

Step	Hyp	Ref	Expression
1		simpr 459	. 2 |- ( ( ta /\ ph ) -> ph )
2		adantl2.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylanl1 648	1 |- ( ( ( ( ta /\ ph ) /\ ps ) /\ 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:  fun11iun  6733  oewordri  7233  sbthlem8  7627  xmulass  11482  caucvgb  13587  clsnsg  20777  metusttoOLD  21229  metustto  21230  constr3cycl  24866  grpoidinvlem3  25409  nmoub3i  25889  riesz3i  27182  csmdsymi  27454  fin2so  30283  heicant  30292  mblfinlem2  30295  mblfinlem3  30296  ismblfin  30298  itg2addnclem  30309  ftc1anclem7  30339  ftc1anc  30341  fzmul  30476  fdc  30481  incsequz2  30485  isbnd3  30523  bndss  30525  ismtyres  30547  rngoisocnv  30627  dirkertrigeq  32125  fourierdlem12  32143  fourierdlem50  32181  fourierdlem103  32234  fourierdlem104  32235  etransclem35  32294