Theorem adantlll 718

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 680	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  753  ad4ant24  754  ad4ant234  1176  fiunlem  7920  sbthlem8  9058  caucvgb  15646  metustto  24441  grpoidinvlem3  30435  nmoub3i  30702  riesz3i  31991  csmdsymi  32263  finxpreclem3  37381  fin2so  37601  matunitlindflem1  37610  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  itg2addnclem  37665  ftc1anclem7  37693  ftc1anc  37695  fzmul  37735  fdc  37739  incsequz2  37743  isbnd3  37778  bndss  37780  ismtyres  37802  rngoisocnv  37975  xralrple2  45350  xralrple3  45370  cvgcaule  45487  limsupmnflem  45718  climrescn  45746  xlimliminflimsup  45860  dirkertrigeq  46099  fourierdlem12  46117  fourierdlem50  46154  fourierdlem103  46207  fourierdlem104  46208  etransclem35  46267  sge0iunmptlemfi  46411  iundjiun  46458  meaiininclem  46484  hoidmvle  46598  ovnhoilem2  46600  smflimlem1  46769  smfrec  46787  smfliminflem  46828