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  7945  sbthlem8  9089  caucvgb  15755  metustto  24761  grpoidinvlem3  30929  nmoub3i  31196  riesz3i  32485  csmdsymi  32757  finxpreclem3  38096  fin2so  38315  matunitlindflem1  38324  mblfinlem2  38366  mblfinlem3  38367  ismblfin  38369  itg2addnclem  38379  ftc1anclem7  38407  ftc1anc  38409  fzmul  38450  fdc  38454  incsequz2  38458  isbnd3  38493  bndss  38495  ismtyres  38517  rngoisocnv  38690  xralrple2  46128  xralrple3  46147  cvgcaule  46263  limsupmnflem  46492  climrescn  46520  xlimliminflimsup  46634  dirkertrigeq  46873  fourierdlem12  46891  fourierdlem50  46928  fourierdlem103  46981  fourierdlem104  46982  etransclem35  47041  sge0iunmptlemfi  47185  iundjiun  47232  meaiininclem  47258  hoidmvle  47372  ovnhoilem2  47374  smflimlem1  47543  smfrec  47561  smfliminflem  47602