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  7900  sbthlem8  9035  caucvgb  15622  metustto  24417  grpoidinvlem3  30408  nmoub3i  30675  riesz3i  31964  csmdsymi  32236  finxpreclem3  37354  fin2so  37574  matunitlindflem1  37583  mblfinlem2  37625  mblfinlem3  37626  ismblfin  37628  itg2addnclem  37638  ftc1anclem7  37666  ftc1anc  37668  fzmul  37708  fdc  37712  incsequz2  37716  isbnd3  37751  bndss  37753  ismtyres  37775  rngoisocnv  37948  xralrple2  45323  xralrple3  45343  cvgcaule  45460  limsupmnflem  45691  climrescn  45719  xlimliminflimsup  45833  dirkertrigeq  46072  fourierdlem12  46090  fourierdlem50  46127  fourierdlem103  46180  fourierdlem104  46181  etransclem35  46240  sge0iunmptlemfi  46384  iundjiun  46431  meaiininclem  46457  hoidmvle  46571  ovnhoilem2  46573  smflimlem1  46742  smfrec  46760  smfliminflem  46801