Theorem adantlll 730

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  ad4ant23  765  ad4ant24  766  ad4ant234  1192  fiunlem  7938  sbthlem8  9081  caucvgb  15730  metustto  24678  grpoidinvlem3  30798  nmoub3i  31065  riesz3i  32354  csmdsymi  32626  finxpreclem3  37926  fin2so  38145  matunitlindflem1  38154  mblfinlem2  38196  mblfinlem3  38197  ismblfin  38199  itg2addnclem  38209  ftc1anclem7  38237  ftc1anc  38239  fzmul  38279  fdc  38283  incsequz2  38287  isbnd3  38322  bndss  38324  ismtyres  38346  rngoisocnv  38519  xralrple2  45961  xralrple3  45980  cvgcaule  46096  limsupmnflem  46325  climrescn  46353  xlimliminflimsup  46467  dirkertrigeq  46706  fourierdlem12  46724  fourierdlem50  46761  fourierdlem103  46814  fourierdlem104  46815  etransclem35  46874  sge0iunmptlemfi  47018  iundjiun  47065  meaiininclem  47091  hoidmvle  47205  ovnhoilem2  47207  smflimlem1  47376  smfrec  47394  smfliminflem  47435