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  1194  fiunlem  7935  sbthlem8  9078  caucvgb  15727  metustto  24710  grpoidinvlem3  30858  nmoub3i  31125  riesz3i  32414  csmdsymi  32686  finxpreclem3  38039  fin2so  38258  matunitlindflem1  38267  mblfinlem2  38309  mblfinlem3  38310  ismblfin  38312  itg2addnclem  38322  ftc1anclem7  38350  ftc1anc  38352  fzmul  38392  fdc  38396  incsequz2  38400  isbnd3  38435  bndss  38437  ismtyres  38459  rngoisocnv  38632  xralrple2  46070  xralrple3  46089  cvgcaule  46205  limsupmnflem  46434  climrescn  46462  xlimliminflimsup  46576  dirkertrigeq  46815  fourierdlem12  46833  fourierdlem50  46870  fourierdlem103  46923  fourierdlem104  46924  etransclem35  46983  sge0iunmptlemfi  47127  iundjiun  47174  meaiininclem  47200  hoidmvle  47314  ovnhoilem2  47316  smflimlem1  47485  smfrec  47503  smfliminflem  47544