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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ad4ant23  753  ad4ant24  754  ad4ant234  1177  fiunlem  7693  sbthlem8  8741  caucvgb  15208  metustto  23405  grpoidinvlem3  28541  nmoub3i  28808  riesz3i  30097  csmdsymi  30369  finxpreclem3  35250  fin2so  35450  matunitlindflem1  35459  mblfinlem2  35501  mblfinlem3  35502  ismblfin  35504  itg2addnclem  35514  ftc1anclem7  35542  ftc1anc  35544  fzmul  35585  fdc  35589  incsequz2  35593  isbnd3  35628  bndss  35630  ismtyres  35652  rngoisocnv  35825  xralrple2  42507  xralrple3  42527  limsupmnflem  42879  climrescn  42907  xlimliminflimsup  43021  dirkertrigeq  43260  fourierdlem12  43278  fourierdlem50  43315  fourierdlem103  43368  fourierdlem104  43369  etransclem35  43428  sge0iunmptlemfi  43569  iundjiun  43616  meaiininclem  43642  hoidmvle  43756  ovnhoilem2  43758  smflimlem1  43921  smfrec  43938  smfliminflem  43978