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  7966  sbthlem8  9130  caucvgb  15716  metustto  24566  grpoidinvlem3  30525  nmoub3i  30792  riesz3i  32081  csmdsymi  32353  finxpreclem3  37394  fin2so  37614  matunitlindflem1  37623  mblfinlem2  37665  mblfinlem3  37666  ismblfin  37668  itg2addnclem  37678  ftc1anclem7  37706  ftc1anc  37708  fzmul  37748  fdc  37752  incsequz2  37756  isbnd3  37791  bndss  37793  ismtyres  37815  rngoisocnv  37988  xralrple2  45365  xralrple3  45385  cvgcaule  45502  limsupmnflem  45735  climrescn  45763  xlimliminflimsup  45877  dirkertrigeq  46116  fourierdlem12  46134  fourierdlem50  46171  fourierdlem103  46224  fourierdlem104  46225  etransclem35  46284  sge0iunmptlemfi  46428  iundjiun  46475  meaiininclem  46501  hoidmvle  46615  ovnhoilem2  46617  smflimlem1  46786  smfrec  46804  smfliminflem  46845