Theorem adantlll 717

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad4ant23  752  ad4ant24  753  ad4ant234  1176  fiunlem  7928  sbthlem8  9090  caucvgb  15626  metustto  24062  grpoidinvlem3  29759  nmoub3i  30026  riesz3i  31315  csmdsymi  31587  finxpreclem3  36274  fin2so  36475  matunitlindflem1  36484  mblfinlem2  36526  mblfinlem3  36527  ismblfin  36529  itg2addnclem  36539  ftc1anclem7  36567  ftc1anc  36569  fzmul  36609  fdc  36613  incsequz2  36617  isbnd3  36652  bndss  36654  ismtyres  36676  rngoisocnv  36849  xralrple2  44064  xralrple3  44084  cvgcaule  44202  limsupmnflem  44436  climrescn  44464  xlimliminflimsup  44578  dirkertrigeq  44817  fourierdlem12  44835  fourierdlem50  44872  fourierdlem103  44925  fourierdlem104  44926  etransclem35  44985  sge0iunmptlemfi  45129  iundjiun  45176  meaiininclem  45202  hoidmvle  45316  ovnhoilem2  45318  smflimlem1  45487  smfrec  45505  smfliminflem  45546