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  7877  sbthlem8  9011  caucvgb  15587  metustto  24439  grpoidinvlem3  30450  nmoub3i  30717  riesz3i  32006  csmdsymi  32278  finxpreclem3  37367  fin2so  37587  matunitlindflem1  37596  mblfinlem2  37638  mblfinlem3  37639  ismblfin  37641  itg2addnclem  37651  ftc1anclem7  37679  ftc1anc  37681  fzmul  37721  fdc  37725  incsequz2  37729  isbnd3  37764  bndss  37766  ismtyres  37788  rngoisocnv  37961  xralrple2  45334  xralrple3  45353  cvgcaule  45470  limsupmnflem  45701  climrescn  45729  xlimliminflimsup  45843  dirkertrigeq  46082  fourierdlem12  46100  fourierdlem50  46137  fourierdlem103  46190  fourierdlem104  46191  etransclem35  46250  sge0iunmptlemfi  46394  iundjiun  46441  meaiininclem  46467  hoidmvle  46581  ovnhoilem2  46583  smflimlem1  46752  smfrec  46770  smfliminflem  46811