Theorem adantlll 714

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 676	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 206  df-an 396

This theorem is referenced by:  ad4ant23  749  ad4ant24  750  ad4ant234  1173  fiunlem  7758  sbthlem8  8830  caucvgb  15319  metustto  23615  grpoidinvlem3  28769  nmoub3i  29036  riesz3i  30325  csmdsymi  30597  finxpreclem3  35491  fin2so  35691  matunitlindflem1  35700  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  itg2addnclem  35755  ftc1anclem7  35783  ftc1anc  35785  fzmul  35826  fdc  35830  incsequz2  35834  isbnd3  35869  bndss  35871  ismtyres  35893  rngoisocnv  36066  xralrple2  42783  xralrple3  42803  limsupmnflem  43151  climrescn  43179  xlimliminflimsup  43293  dirkertrigeq  43532  fourierdlem12  43550  fourierdlem50  43587  fourierdlem103  43640  fourierdlem104  43641  etransclem35  43700  sge0iunmptlemfi  43841  iundjiun  43888  meaiininclem  43914  hoidmvle  44028  ovnhoilem2  44030  smflimlem1  44193  smfrec  44210  smfliminflem  44250