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  7886  sbthlem8  9022  caucvgb  15603  metustto  24497  grpoidinvlem3  30581  nmoub3i  30848  riesz3i  32137  csmdsymi  32409  finxpreclem3  37598  fin2so  37808  matunitlindflem1  37817  mblfinlem2  37859  mblfinlem3  37860  ismblfin  37862  itg2addnclem  37872  ftc1anclem7  37900  ftc1anc  37902  fzmul  37942  fdc  37946  incsequz2  37950  isbnd3  37985  bndss  37987  ismtyres  38009  rngoisocnv  38182  xralrple2  45599  xralrple3  45618  cvgcaule  45735  limsupmnflem  45964  climrescn  45992  xlimliminflimsup  46106  dirkertrigeq  46345  fourierdlem12  46363  fourierdlem50  46400  fourierdlem103  46453  fourierdlem104  46454  etransclem35  46513  sge0iunmptlemfi  46657  iundjiun  46704  meaiininclem  46730  hoidmvle  46844  ovnhoilem2  46846  smflimlem1  47015  smfrec  47033  smfliminflem  47074