Theorem adantlll 731

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4ant23  766  ad4ant24  767  ad4ant234  1194  fiunlem  7956  sbthlem8  9118  caucvgb  15854  matunitlindflem1  23001  metustto  24879  grpoidinvlem3  31115  nmoub3i  31382  riesz3i  32671  csmdsymi  32943  finxpreclem3  38423  fin2so  38637  mblfinlem2  38683  mblfinlem3  38684  ismblfin  38686  itg2addnclem  38696  ftc1anclem7  38724  ftc1anc  38726  fzmul  38782  fdc  38786  incsequz2  38790  isbnd3  38825  bndss  38827  ismtyres  38849  rngoisocnv  39022  xralrple2  46473  xralrple3  46492  cvgcaule  46608  limsupmnflem  46837  climrescn  46865  xlimliminflimsup  46979  dirkertrigeq  47218  fourierdlem12  47236  fourierdlem50  47273  fourierdlem103  47326  fourierdlem104  47327  etransclem35  47386  sge0iunmptlemfi  47530  iundjiun  47577  meaiininclem  47603  hoidmvle  47717  ovnhoilem2  47719  smflimlem1  47888  smfrec  47906  smfliminflem  47947