Theorem adantlll 716

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ad4ant23  751  ad4ant24  752  ad4ant234  1175  fiunlem  7924  sbthlem8  9086  caucvgb  15622  metustto  24053  grpoidinvlem3  29746  nmoub3i  30013  riesz3i  31302  csmdsymi  31574  finxpreclem3  36262  fin2so  36463  matunitlindflem1  36472  mblfinlem2  36514  mblfinlem3  36515  ismblfin  36517  itg2addnclem  36527  ftc1anclem7  36555  ftc1anc  36557  fzmul  36597  fdc  36601  incsequz2  36605  isbnd3  36640  bndss  36642  ismtyres  36664  rngoisocnv  36837  xralrple2  44050  xralrple3  44070  cvgcaule  44188  limsupmnflem  44422  climrescn  44450  xlimliminflimsup  44564  dirkertrigeq  44803  fourierdlem12  44821  fourierdlem50  44858  fourierdlem103  44911  fourierdlem104  44912  etransclem35  44971  sge0iunmptlemfi  45115  iundjiun  45162  meaiininclem  45188  hoidmvle  45302  ovnhoilem2  45304  smflimlem1  45473  smfrec  45491  smfliminflem  45532