Theorem adantlll 714

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad4ant23  749  ad4ant24  750  ad4ant234  1168  fiunlem  7506  sbthlem8  8488  caucvgb  14874  metustto  22850  grpoidinvlem3  27970  nmoub3i  28237  riesz3i  29526  csmdsymi  29798  finxpreclem3  34226  fin2so  34431  matunitlindflem1  34440  mblfinlem2  34482  mblfinlem3  34483  ismblfin  34485  itg2addnclem  34495  ftc1anclem7  34525  ftc1anc  34527  fzmul  34569  fdc  34573  incsequz2  34577  isbnd3  34615  bndss  34617  ismtyres  34639  rngoisocnv  34812  xralrple2  41184  xralrple3  41204  limsupmnflem  41564  climrescn  41592  xlimliminflimsup  41706  dirkertrigeq  41950  fourierdlem12  41968  fourierdlem50  42005  fourierdlem103  42058  fourierdlem104  42059  etransclem35  42118  sge0iunmptlemfi  42259  iundjiun  42306  meaiininclem  42332  hoidmvle  42446  ovnhoilem2  42448  smflimlem1  42611  smfrec  42628  smfliminflem  42668