Theorem sylanl2 686

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  mpanlr1  724  adantlrl  758  adantlrr  759  oesuclem  7772  oelim  7781  mulsub  10663  divsubdiv  10931  lcmneg  15516  vdwlem12  15896  dpjidcl  18655  mplbas2  19670  monmat2matmon  20829  bwth  21413  cnextfun  22067  elbl4  22567  metucn  22575  dvradcnv  24372  dchrisum0lem2a  25403  axcontlem4  26044  cnlnadjlem2  29234  chirredlem2  29557  mdsymlem5  29573  sibfof  30709  relowlssretop  33520  matunitlindflem1  33716  poimirlem29  33749  unichnidl  34141  dmncan2  34187  cvrexchlem  35206  jm2.26  38069  radcnvrat  39013  binomcxplemnotnn0  39055  suplesup  40051  dvnmptdivc  40654  fourierdlem64  40888  fourierdlem74  40898  fourierdlem75  40899  fourierdlem83  40907  etransclem35  40987  iundjiun  41178  hoidmvlelem2  41314