Theorem adantlll 731

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4ant23  766  ad4ant24  767  ad4ant234  1194  fiunlem  7988  sbthlem8  9151  caucvgb  15891  matunitlindflem1  23049  metustto  24927  grpoidinvlem3  31165  nmoub3i  31432  riesz3i  32721  csmdsymi  32993  finxpreclem3  38584  fin2so  38798  mblfinlem2  38844  mblfinlem3  38845  ismblfin  38847  itg2addnclem  38857  ftc1anclem7  38885  ftc1anc  38887  fzmul  38941  fdc  38945  incsequz2  38949  isbnd3  38984  bndss  38986  ismtyres  39008  rngoisocnv  39181  xralrple2  46639  xralrple3  46658  cvgcaule  46774  limsupmnflem  47003  climrescn  47031  xlimliminflimsup  47145  dirkertrigeq  47384  fourierdlem12  47402  fourierdlem50  47439  fourierdlem103  47492  fourierdlem104  47493  etransclem35  47552  sge0iunmptlemfi  47696  iundjiun  47743  meaiininclem  47769  hoidmvle  47883  ovnhoilem2  47885  smflimlem1  48054  smfrec  48072  smfliminflem  48113