Theorem adantlll 750

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 476	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 680	1 ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  fun11iun  7019  oewordri  7559  sbthlem8  7962  xmulass  11989  caucvgb  14258  clsnsg  21723  metustto  22168  constr3cycl  26189  grpoidinvlem3  26744  nmoub3i  27012  riesz3i  28305  csmdsymi  28577  finxpreclem3  32406  fin2so  32566  matunitlindflem1  32575  mblfinlem2  32617  mblfinlem3  32618  ismblfin  32620  itg2addnclem  32631  ftc1anclem7  32661  ftc1anc  32663  fzmul  32707  fdc  32711  incsequz2  32715  isbnd3  32753  bndss  32755  ismtyres  32777  rngoisocnv  32950  xralrple2  38511  xralrple3  38531  dirkertrigeq  38994  fourierdlem12  39012  fourierdlem50  39049  fourierdlem103  39102  fourierdlem104  39103  etransclem35  39162  sge0iunmptlemfi  39306  iundjiun  39353  meaiininclem  39376  hoidmvle  39490  ovnhoilem2  39492  smflimlem1  39657  smfrec  39674