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  15582  metustto  24463  grpoidinvlem3  30478  nmoub3i  30745  riesz3i  32034  csmdsymi  32306  finxpreclem3  37427  fin2so  37647  matunitlindflem1  37656  mblfinlem2  37698  mblfinlem3  37699  ismblfin  37701  itg2addnclem  37711  ftc1anclem7  37739  ftc1anc  37741  fzmul  37781  fdc  37785  incsequz2  37789  isbnd3  37824  bndss  37826  ismtyres  37848  rngoisocnv  38021  xralrple2  45393  xralrple3  45412  cvgcaule  45529  limsupmnflem  45758  climrescn  45786  xlimliminflimsup  45900  dirkertrigeq  46139  fourierdlem12  46157  fourierdlem50  46194  fourierdlem103  46247  fourierdlem104  46248  etransclem35  46307  sge0iunmptlemfi  46451  iundjiun  46498  meaiininclem  46524  hoidmvle  46638  ovnhoilem2  46640  smflimlem1  46809  smfrec  46827  smfliminflem  46868