Theorem adantlll 719

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad4ant23  754  ad4ant24  755  ad4ant234  1177  fiunlem  7896  sbthlem8  9034  caucvgb  15615  metustto  24509  grpoidinvlem3  30594  nmoub3i  30861  riesz3i  32150  csmdsymi  32422  finxpreclem3  37648  fin2so  37858  matunitlindflem1  37867  mblfinlem2  37909  mblfinlem3  37910  ismblfin  37912  itg2addnclem  37922  ftc1anclem7  37950  ftc1anc  37952  fzmul  37992  fdc  37996  incsequz2  38000  isbnd3  38035  bndss  38037  ismtyres  38059  rngoisocnv  38232  xralrple2  45713  xralrple3  45732  cvgcaule  45849  limsupmnflem  46078  climrescn  46106  xlimliminflimsup  46220  dirkertrigeq  46459  fourierdlem12  46477  fourierdlem50  46514  fourierdlem103  46567  fourierdlem104  46568  etransclem35  46627  sge0iunmptlemfi  46771  iundjiun  46818  meaiininclem  46844  hoidmvle  46958  ovnhoilem2  46960  smflimlem1  47129  smfrec  47147  smfliminflem  47188