Theorem adantlll 718

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 680	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  753  ad4ant24  754  ad4ant234  1174  fiunlem  7964  sbthlem8  9128  caucvgb  15712  metustto  24581  grpoidinvlem3  30534  nmoub3i  30801  riesz3i  32090  csmdsymi  32362  finxpreclem3  37375  fin2so  37593  matunitlindflem1  37602  mblfinlem2  37644  mblfinlem3  37645  ismblfin  37647  itg2addnclem  37657  ftc1anclem7  37685  ftc1anc  37687  fzmul  37727  fdc  37731  incsequz2  37735  isbnd3  37770  bndss  37772  ismtyres  37794  rngoisocnv  37967  xralrple2  45303  xralrple3  45323  cvgcaule  45441  limsupmnflem  45675  climrescn  45703  xlimliminflimsup  45817  dirkertrigeq  46056  fourierdlem12  46074  fourierdlem50  46111  fourierdlem103  46164  fourierdlem104  46165  etransclem35  46224  sge0iunmptlemfi  46368  iundjiun  46415  meaiininclem  46441  hoidmvle  46555  ovnhoilem2  46557  smflimlem1  46726  smfrec  46744  smfliminflem  46785