Theorem adantlll 716

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 678	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 206  df-an 397

This theorem is referenced by:  ad4ant23  751  ad4ant24  752  ad4ant234  1175  fiunlem  7930  sbthlem8  9092  caucvgb  15628  metustto  24069  grpoidinvlem3  29797  nmoub3i  30064  riesz3i  31353  csmdsymi  31625  finxpreclem3  36360  fin2so  36561  matunitlindflem1  36570  mblfinlem2  36612  mblfinlem3  36613  ismblfin  36615  itg2addnclem  36625  ftc1anclem7  36653  ftc1anc  36655  fzmul  36695  fdc  36699  incsequz2  36703  isbnd3  36738  bndss  36740  ismtyres  36762  rngoisocnv  36935  xralrple2  44143  xralrple3  44163  cvgcaule  44281  limsupmnflem  44515  climrescn  44543  xlimliminflimsup  44657  dirkertrigeq  44896  fourierdlem12  44914  fourierdlem50  44951  fourierdlem103  45004  fourierdlem104  45005  etransclem35  45064  sge0iunmptlemfi  45208  iundjiun  45255  meaiininclem  45281  hoidmvle  45395  ovnhoilem2  45397  smflimlem1  45566  smfrec  45584  smfliminflem  45625