Theorem sylanl2 680

Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
sylanl2.1	⊢ (𝜑 → 𝜒)
sylanl2.2	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
sylanl2	⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl2

Step	Hyp	Ref	Expression
1		sylanl2.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantl 485	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	syldanl 604	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 210  df-an 400

This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  7778  2ndconst  7779  oesuclem  8133  oelim  8142  mulsub  11072  divsubdiv  11345  lcmneg  15937  vdwlem12  16318  dpjidcl  19173  mplbas2  20710  monmat2matmon  21429  bwth  22015  cnextfun  22669  elbl4  23170  metucn  23178  dvradcnv  25016  dchrisum0lem2a  26101  axcontlem4  26761  cnlnadjlem2  29851  chirredlem2  30174  mdsymlem5  30190  sibfof  31708  relowlssretop  34780  matunitlindflem1  35053  poimirlem29  35086  unichnidl  35469  dmncan2  35515  cvrexchlem  36715  jm2.26  39943  radcnvrat  41018  binomcxplemnotnn0  41060  suplesup  41971  dvnmptdivc  42580  fourierdlem64  42812  fourierdlem74  42822  fourierdlem75  42823  fourierdlem83  42831  etransclem35  42911  iundjiun  43099  hoidmvlelem2  43235