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  1176  fiunlem  7869  sbthlem8  9002  caucvgb  15579  metustto  24461  grpoidinvlem3  30476  nmoub3i  30743  riesz3i  32032  csmdsymi  32304  finxpreclem3  37406  fin2so  37626  matunitlindflem1  37635  mblfinlem2  37677  mblfinlem3  37678  ismblfin  37680  itg2addnclem  37690  ftc1anclem7  37718  ftc1anc  37720  fzmul  37760  fdc  37764  incsequz2  37768  isbnd3  37803  bndss  37805  ismtyres  37827  rngoisocnv  38000  xralrple2  45372  xralrple3  45391  cvgcaule  45508  limsupmnflem  45737  climrescn  45765  xlimliminflimsup  45879  dirkertrigeq  46118  fourierdlem12  46136  fourierdlem50  46173  fourierdlem103  46226  fourierdlem104  46227  etransclem35  46286  sge0iunmptlemfi  46430  iundjiun  46477  meaiininclem  46503  hoidmvle  46617  ovnhoilem2  46619  smflimlem1  46788  smfrec  46806  smfliminflem  46847