Theorem sylanl2 694

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanlr1  719  adantlrl  733  adantlrr  734  1stconst  8104  2ndconst  8105  oesuclem  8519  oelim  8528  undom  9063  mulsub  11675  divsubdiv  11949  lcmneg  16686  vdwlem12  17077  dpjidcl  20161  mplbas2  22230  evlsvvval  22281  monmat2matmon  23018  bwth  23604  cnextfun  24258  elbl4  24757  metucn  24765  dvradcnv  26621  dchrisum0lem2a  27718  axcontlem4  29354  cnlnadjlem2  32457  chirredlem2  32780  mdsymlem5  32796  sibfof  34762  fineqvnttrclselem1  35558  relowlssretop  38050  matunitlindflem1  38308  poimirlem29  38341  unichnidl  38723  dmncan2  38769  cvrexchlem  40234  jm2.26  43770  radcnvrat  45065  binomcxplemnotnn0  45107  suplesup  46096  dvnmptdivc  46693  fourierdlem64  46925  fourierdlem74  46935  fourierdlem75  46936  fourierdlem83  46944  etransclem35  47024  iundjiun  47215  hoidmvlelem2  47351  idomcanr  49154