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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad4ant23  753  ad4ant24  754  ad4ant234  1176  fiunlem  7923  sbthlem8  9064  caucvgb  15653  metustto  24448  grpoidinvlem3  30442  nmoub3i  30709  riesz3i  31998  csmdsymi  32270  finxpreclem3  37388  fin2so  37608  matunitlindflem1  37617  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  itg2addnclem  37672  ftc1anclem7  37700  ftc1anc  37702  fzmul  37742  fdc  37746  incsequz2  37750  isbnd3  37785  bndss  37787  ismtyres  37809  rngoisocnv  37982  xralrple2  45357  xralrple3  45377  cvgcaule  45494  limsupmnflem  45725  climrescn  45753  xlimliminflimsup  45867  dirkertrigeq  46106  fourierdlem12  46124  fourierdlem50  46161  fourierdlem103  46214  fourierdlem104  46215  etransclem35  46274  sge0iunmptlemfi  46418  iundjiun  46465  meaiininclem  46491  hoidmvle  46605  ovnhoilem2  46607  smflimlem1  46776  smfrec  46794  smfliminflem  46835