Theorem adantlll 730

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad4ant23  765  ad4ant24  766  ad4ant234  1192  fiunlem  7939  sbthlem8  9082  caucvgb  15731  metustto  24679  grpoidinvlem3  30799  nmoub3i  31066  riesz3i  32355  csmdsymi  32627  finxpreclem3  37962  fin2so  38181  matunitlindflem1  38190  mblfinlem2  38232  mblfinlem3  38233  ismblfin  38235  itg2addnclem  38245  ftc1anclem7  38273  ftc1anc  38275  fzmul  38315  fdc  38319  incsequz2  38323  isbnd3  38358  bndss  38360  ismtyres  38382  rngoisocnv  38555  xralrple2  45997  xralrple3  46016  cvgcaule  46132  limsupmnflem  46361  climrescn  46389  xlimliminflimsup  46503  dirkertrigeq  46742  fourierdlem12  46760  fourierdlem50  46797  fourierdlem103  46850  fourierdlem104  46851  etransclem35  46910  sge0iunmptlemfi  47054  iundjiun  47101  meaiininclem  47127  hoidmvle  47241  ovnhoilem2  47243  smflimlem1  47412  smfrec  47430  smfliminflem  47471