Theorem adantlll 731

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4ant23  766  ad4ant24  767  ad4ant234  1194  fiunlem  7939  sbthlem8  9092  caucvgb  15767  matunitlindflem1  22901  metustto  24779  grpoidinvlem3  30987  nmoub3i  31254  riesz3i  32543  csmdsymi  32815  finxpreclem3  38147  fin2so  38361  mblfinlem2  38407  mblfinlem3  38408  ismblfin  38410  itg2addnclem  38420  ftc1anclem7  38448  ftc1anc  38450  fzmul  38491  fdc  38495  incsequz2  38499  isbnd3  38534  bndss  38536  ismtyres  38558  rngoisocnv  38731  xralrple2  46184  xralrple3  46203  cvgcaule  46319  limsupmnflem  46548  climrescn  46576  xlimliminflimsup  46690  dirkertrigeq  46929  fourierdlem12  46947  fourierdlem50  46984  fourierdlem103  47037  fourierdlem104  47038  etransclem35  47097  sge0iunmptlemfi  47241  iundjiun  47288  meaiininclem  47314  hoidmvle  47428  ovnhoilem2  47430  smflimlem1  47599  smfrec  47617  smfliminflem  47658