Theorem adantlll 719

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 681	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  754  ad4ant24  755  ad4ant234  1177  fiunlem  7895  sbthlem8  9032  caucvgb  15642  metustto  24518  grpoidinvlem3  30577  nmoub3i  30844  riesz3i  32133  csmdsymi  32405  finxpreclem3  37709  fin2so  37928  matunitlindflem1  37937  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  itg2addnclem  37992  ftc1anclem7  38020  ftc1anc  38022  fzmul  38062  fdc  38066  incsequz2  38070  isbnd3  38105  bndss  38107  ismtyres  38129  rngoisocnv  38302  xralrple2  45784  xralrple3  45803  cvgcaule  45919  limsupmnflem  46148  climrescn  46176  xlimliminflimsup  46290  dirkertrigeq  46529  fourierdlem12  46547  fourierdlem50  46584  fourierdlem103  46637  fourierdlem104  46638  etransclem35  46697  sge0iunmptlemfi  46841  iundjiun  46888  meaiininclem  46914  hoidmvle  47028  ovnhoilem2  47030  smflimlem1  47199  smfrec  47217  smfliminflem  47258