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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ad4ant23  751  ad4ant24  752  ad4ant234  1170  fiunlem  7635  sbthlem8  8626  caucvgb  15028  metustto  23155  grpoidinvlem3  28275  nmoub3i  28542  riesz3i  29831  csmdsymi  30103  finxpreclem3  34666  fin2so  34871  matunitlindflem1  34880  mblfinlem2  34922  mblfinlem3  34923  ismblfin  34925  itg2addnclem  34935  ftc1anclem7  34965  ftc1anc  34967  fzmul  35008  fdc  35012  incsequz2  35016  isbnd3  35054  bndss  35056  ismtyres  35078  rngoisocnv  35251  xralrple2  41612  xralrple3  41632  limsupmnflem  41991  climrescn  42019  xlimliminflimsup  42133  dirkertrigeq  42377  fourierdlem12  42395  fourierdlem50  42432  fourierdlem103  42485  fourierdlem104  42486  etransclem35  42545  sge0iunmptlemfi  42686  iundjiun  42733  meaiininclem  42759  hoidmvle  42873  ovnhoilem2  42875  smflimlem1  43038  smfrec  43055  smfliminflem  43095