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  8113  2ndconst  8114  oesuclem  8536  oelim  8545  undom  9087  mulsub  11762  divsubdiv  12036  lcmneg  16783  vdwlem12  17175  dpjidcl  20279  mplbas2  22356  evlsvvval  22407  matunitlindflem1  22999  monmat2matmon  23147  bwth  23733  cnextfun  24388  elbl4  24887  metucn  24895  dvradcnv  26753  dchrisum0lem2a  27849  axcontlem4  29550  cnlnadjlem2  32675  chirredlem2  32998  mdsymlem5  33014  sibfof  35018  fineqvnttrclselem1  35845  relowlssretop  38379  poimirlem29  38660  unichnidl  39058  dmncan2  39104  cvrexchlem  40569  jm2.26  44102  radcnvrat  45391  binomcxplemnotnn0  45433  suplesup  46444  dvnmptdivc  47041  fourierdlem64  47273  fourierdlem74  47283  fourierdlem75  47284  fourierdlem83  47292  etransclem35  47372  iundjiun  47563  hoidmvlelem2  47699  idomcanr  49538