Theorem adantlll 728

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 690	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 209  df-an 400

This theorem is referenced by:  ad4ant23  763  ad4ant24  764  ad4ant234  1188  fiunlem  7918  sbthlem8  9060  caucvgb  15698  metustto  24601  grpoidinvlem3  30666  nmoub3i  30933  riesz3i  32222  csmdsymi  32494  finxpreclem3  37848  fin2so  38067  matunitlindflem1  38076  mblfinlem2  38118  mblfinlem3  38119  ismblfin  38121  itg2addnclem  38131  ftc1anclem7  38159  ftc1anc  38161  fzmul  38201  fdc  38205  incsequz2  38209  isbnd3  38244  bndss  38246  ismtyres  38268  rngoisocnv  38441  xralrple2  45891  xralrple3  45910  cvgcaule  46026  limsupmnflem  46255  climrescn  46283  xlimliminflimsup  46397  dirkertrigeq  46636  fourierdlem12  46654  fourierdlem50  46691  fourierdlem103  46744  fourierdlem104  46745  etransclem35  46804  sge0iunmptlemfi  46948  iundjiun  46995  meaiininclem  47021  hoidmvle  47135  ovnhoilem2  47137  smflimlem1  47306  smfrec  47324  smfliminflem  47365