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 484	. 2 ⊢ ((𝜏 ∧ 𝜑) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 679	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  752  ad4ant24  753  ad4ant234  1175  fiunlem  7982  sbthlem8  9156  caucvgb  15728  metustto  24587  grpoidinvlem3  30538  nmoub3i  30805  riesz3i  32094  csmdsymi  32366  finxpreclem3  37359  fin2so  37567  matunitlindflem1  37576  mblfinlem2  37618  mblfinlem3  37619  ismblfin  37621  itg2addnclem  37631  ftc1anclem7  37659  ftc1anc  37661  fzmul  37701  fdc  37705  incsequz2  37709  isbnd3  37744  bndss  37746  ismtyres  37768  rngoisocnv  37941  xralrple2  45269  xralrple3  45289  cvgcaule  45407  limsupmnflem  45641  climrescn  45669  xlimliminflimsup  45783  dirkertrigeq  46022  fourierdlem12  46040  fourierdlem50  46077  fourierdlem103  46130  fourierdlem104  46131  etransclem35  46190  sge0iunmptlemfi  46334  iundjiun  46381  meaiininclem  46407  hoidmvle  46521  ovnhoilem2  46523  smflimlem1  46692  smfrec  46710  smfliminflem  46751