Theorem adantlll 724

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 686	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 208  df-an 397

This theorem is referenced by:  ad4ant23  759  ad4ant24  760  ad4ant234  1182  fiunlem  7884  sbthlem8  9022  caucvgb  15633  metustto  24536  grpoidinvlem3  30595  nmoub3i  30862  riesz3i  32151  csmdsymi  32423  finxpreclem3  37755  fin2so  37974  matunitlindflem1  37983  mblfinlem2  38025  mblfinlem3  38026  ismblfin  38028  itg2addnclem  38038  ftc1anclem7  38066  ftc1anc  38068  fzmul  38108  fdc  38112  incsequz2  38116  isbnd3  38151  bndss  38153  ismtyres  38175  rngoisocnv  38348  xralrple2  45799  xralrple3  45818  cvgcaule  45934  limsupmnflem  46163  climrescn  46191  xlimliminflimsup  46305  dirkertrigeq  46544  fourierdlem12  46562  fourierdlem50  46599  fourierdlem103  46652  fourierdlem104  46653  etransclem35  46712  sge0iunmptlemfi  46856  iundjiun  46903  meaiininclem  46929  hoidmvle  47043  ovnhoilem2  47045  smflimlem1  47214  smfrec  47232  smfliminflem  47273