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  8100  2ndconst  8101  oesuclem  8517  oelim  8526  undom  9068  mulsub  11740  divsubdiv  12014  lcmneg  16758  vdwlem12  17150  dpjidcl  20254  mplbas2  22331  evlsvvval  22382  matunitlindflem1  22974  monmat2matmon  23122  bwth  23708  cnextfun  24363  elbl4  24862  metucn  24870  dvradcnv  26730  dchrisum0lem2a  27826  axcontlem4  29527  cnlnadjlem2  32652  chirredlem2  32975  mdsymlem5  32991  sibfof  34955  fineqvnttrclselem1  35762  relowlssretop  38254  poimirlem29  38535  unichnidl  38933  dmncan2  38979  cvrexchlem  40444  jm2.26  43962  radcnvrat  45257  binomcxplemnotnn0  45299  suplesup  46295  dvnmptdivc  46892  fourierdlem64  47124  fourierdlem74  47134  fourierdlem75  47135  fourierdlem83  47143  etransclem35  47223  iundjiun  47414  hoidmvlelem2  47550  idomcanr  49389