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	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantlll	⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlll

Step	Hyp	Ref	Expression
1		simpr 485	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 677	1 ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad4ant23  750  ad4ant24  751  ad4ant234  1174  fiunlem  7793  sbthlem8  8886  caucvgb  15400  metustto  23718  grpoidinvlem3  28877  nmoub3i  29144  riesz3i  30433  csmdsymi  30705  finxpreclem3  35573  fin2so  35773  matunitlindflem1  35782  mblfinlem2  35824  mblfinlem3  35825  ismblfin  35827  itg2addnclem  35837  ftc1anclem7  35865  ftc1anc  35867  fzmul  35908  fdc  35912  incsequz2  35916  isbnd3  35951  bndss  35953  ismtyres  35975  rngoisocnv  36148  xralrple2  42900  xralrple3  42920  limsupmnflem  43268  climrescn  43296  xlimliminflimsup  43410  dirkertrigeq  43649  fourierdlem12  43667  fourierdlem50  43704  fourierdlem103  43757  fourierdlem104  43758  etransclem35  43817  sge0iunmptlemfi  43958  iundjiun  44005  meaiininclem  44031  hoidmvle  44145  ovnhoilem2  44147  smflimlem1  44316  smfrec  44334  smfliminflem  44374