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  7952  sbthlem8  9106  caucvgb  15840  matunitlindflem1  22987  metustto  24865  grpoidinvlem3  31101  nmoub3i  31368  riesz3i  32657  csmdsymi  32929  finxpreclem3  38296  fin2so  38510  mblfinlem2  38556  mblfinlem3  38557  ismblfin  38559  itg2addnclem  38569  ftc1anclem7  38597  ftc1anc  38599  fzmul  38655  fdc  38659  incsequz2  38663  isbnd3  38698  bndss  38700  ismtyres  38722  rngoisocnv  38895  xralrple2  46335  xralrple3  46354  cvgcaule  46470  limsupmnflem  46699  climrescn  46727  xlimliminflimsup  46841  dirkertrigeq  47080  fourierdlem12  47098  fourierdlem50  47135  fourierdlem103  47188  fourierdlem104  47189  etransclem35  47248  sge0iunmptlemfi  47392  iundjiun  47439  meaiininclem  47465  hoidmvle  47579  ovnhoilem2  47581  smflimlem1  47750  smfrec  47768  smfliminflem  47809