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  7883  sbthlem8  9018  caucvgb  15594  metustto  24488  grpoidinvlem3  30507  nmoub3i  30774  riesz3i  32063  csmdsymi  32335  finxpreclem3  37510  fin2so  37720  matunitlindflem1  37729  mblfinlem2  37771  mblfinlem3  37772  ismblfin  37774  itg2addnclem  37784  ftc1anclem7  37812  ftc1anc  37814  fzmul  37854  fdc  37858  incsequz2  37862  isbnd3  37897  bndss  37899  ismtyres  37921  rngoisocnv  38094  xralrple2  45515  xralrple3  45534  cvgcaule  45651  limsupmnflem  45880  climrescn  45908  xlimliminflimsup  46022  dirkertrigeq  46261  fourierdlem12  46279  fourierdlem50  46316  fourierdlem103  46369  fourierdlem104  46370  etransclem35  46429  sge0iunmptlemfi  46573  iundjiun  46620  meaiininclem  46646  hoidmvle  46760  ovnhoilem2  46762  smflimlem1  46931  smfrec  46949  smfliminflem  46990