Theorem adantlll 754

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  fun11iun  7126  oewordri  7672  sbthlem8  8077  xmulass  12117  caucvgb  14410  clsnsg  21913  metustto  22358  grpoidinvlem3  27360  nmoub3i  27628  riesz3i  28921  csmdsymi  29193  finxpreclem3  33230  fin2so  33396  matunitlindflem1  33405  mblfinlem2  33447  mblfinlem3  33448  ismblfin  33450  itg2addnclem  33461  ftc1anclem7  33491  ftc1anc  33493  fzmul  33537  fdc  33541  incsequz2  33545  isbnd3  33583  bndss  33585  ismtyres  33607  rngoisocnv  33780  xralrple2  39570  xralrple3  39590  limsupmnflem  39952  climrescn  39980  dirkertrigeq  40318  fourierdlem12  40336  fourierdlem50  40373  fourierdlem103  40426  fourierdlem104  40427  etransclem35  40486  sge0iunmptlemfi  40630  iundjiun  40677  meaiininclem  40700  hoidmvle  40814  ovnhoilem2  40816  smflimlem1  40979  smfrec  40996  smfliminflem  41036