Theorem adantlll 728

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad4ant23  763  ad4ant24  764  ad4ant234  1189  fiunlem  7923  sbthlem8  9066  caucvgb  15707  metustto  24610  grpoidinvlem3  30706  nmoub3i  30973  riesz3i  32262  csmdsymi  32534  finxpreclem3  37884  fin2so  38103  matunitlindflem1  38112  mblfinlem2  38154  mblfinlem3  38155  ismblfin  38157  itg2addnclem  38167  ftc1anclem7  38195  ftc1anc  38197  fzmul  38237  fdc  38241  incsequz2  38245  isbnd3  38280  bndss  38282  ismtyres  38304  rngoisocnv  38477  xralrple2  45927  xralrple3  45946  cvgcaule  46062  limsupmnflem  46291  climrescn  46319  xlimliminflimsup  46433  dirkertrigeq  46672  fourierdlem12  46690  fourierdlem50  46727  fourierdlem103  46780  fourierdlem104  46781  etransclem35  46840  sge0iunmptlemfi  46984  iundjiun  47031  meaiininclem  47057  hoidmvle  47171  ovnhoilem2  47173  smflimlem1  47342  smfrec  47360  smfliminflem  47401