Theorem adantlll 718

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 680	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  753  ad4ant24  754  ad4ant234  1176  fiunlem  7940  sbthlem8  9104  caucvgb  15696  metustto  24492  grpoidinvlem3  30487  nmoub3i  30754  riesz3i  32043  csmdsymi  32315  finxpreclem3  37411  fin2so  37631  matunitlindflem1  37640  mblfinlem2  37682  mblfinlem3  37683  ismblfin  37685  itg2addnclem  37695  ftc1anclem7  37723  ftc1anc  37725  fzmul  37765  fdc  37769  incsequz2  37773  isbnd3  37808  bndss  37810  ismtyres  37832  rngoisocnv  38005  xralrple2  45381  xralrple3  45401  cvgcaule  45518  limsupmnflem  45749  climrescn  45777  xlimliminflimsup  45891  dirkertrigeq  46130  fourierdlem12  46148  fourierdlem50  46185  fourierdlem103  46238  fourierdlem104  46239  etransclem35  46298  sge0iunmptlemfi  46442  iundjiun  46489  meaiininclem  46515  hoidmvle  46629  ovnhoilem2  46631  smflimlem1  46800  smfrec  46818  smfliminflem  46859