Theorem adantlll 719

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 681	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  754  ad4ant24  755  ad4ant234  1177  fiunlem  7888  sbthlem8  9025  caucvgb  15633  metustto  24528  grpoidinvlem3  30592  nmoub3i  30859  riesz3i  32148  csmdsymi  32420  finxpreclem3  37723  fin2so  37942  matunitlindflem1  37951  mblfinlem2  37993  mblfinlem3  37994  ismblfin  37996  itg2addnclem  38006  ftc1anclem7  38034  ftc1anc  38036  fzmul  38076  fdc  38080  incsequz2  38084  isbnd3  38119  bndss  38121  ismtyres  38143  rngoisocnv  38316  xralrple2  45802  xralrple3  45821  cvgcaule  45937  limsupmnflem  46166  climrescn  46194  xlimliminflimsup  46308  dirkertrigeq  46547  fourierdlem12  46565  fourierdlem50  46602  fourierdlem103  46655  fourierdlem104  46656  etransclem35  46715  sge0iunmptlemfi  46859  iundjiun  46906  meaiininclem  46932  hoidmvle  47046  ovnhoilem2  47048  smflimlem1  47217  smfrec  47235  smfliminflem  47276