Theorem sylanl2 683

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

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  mpanlr1  722  adantlrl  756  adantlrr  757  oesuclem  7605  oelim  7614  mulsub  10473  divsubdiv  10741  lcmneg  15316  vdwlem12  15696  dpjidcl  18457  mplbas2  19470  monmat2matmon  20629  bwth  21213  cnextfun  21868  elbl4  22368  metucn  22376  dvradcnv  24175  dchrisum0lem2a  25206  axcontlem4  25847  cnlnadjlem2  28927  chirredlem2  29250  mdsymlem5  29266  sibfof  30402  relowlssretop  33211  matunitlindflem1  33405  poimirlem29  33438  unichnidl  33830  dmncan2  33876  cvrexchlem  34705  jm2.26  37569  radcnvrat  38513  binomcxplemnotnn0  38555  suplesup  39555  dvnmptdivc  40153  fourierdlem64  40387  fourierdlem74  40397  fourierdlem75  40398  fourierdlem83  40406  etransclem35  40486  iundjiun  40677  hoidmvlelem2  40810