Theorem sylanl2 672

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	anim2i 611	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 576	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  mpanlr1  698  adantlrl  712  adantlrr  713  1stconst  7502  2ndconst  7503  oesuclem  7845  oelim  7854  mulsub  10765  divsubdiv  11033  lcmneg  15651  vdwlem12  16029  dpjidcl  18773  mplbas2  19793  monmat2matmon  20957  bwth  21542  cnextfun  22196  elbl4  22696  metucn  22704  dvradcnv  24516  dchrisum0lem2a  25558  axcontlem4  26204  cnlnadjlem2  29452  chirredlem2  29775  mdsymlem5  29791  sibfof  30918  relowlssretop  33709  matunitlindflem1  33894  poimirlem29  33927  unichnidl  34317  dmncan2  34363  cvrexchlem  35440  jm2.26  38354  radcnvrat  39295  binomcxplemnotnn0  39337  suplesup  40299  dvnmptdivc  40897  fourierdlem64  41130  fourierdlem74  41140  fourierdlem75  41141  fourierdlem83  41149  etransclem35  41229  iundjiun  41420  hoidmvlelem2  41556