Theorem sylanl2 681

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanlr1  706  adantlrl  720  adantlrr  721  1stconst  8125  2ndconst  8126  oesuclem  8563  oelim  8572  undom  9099  mulsub  11706  divsubdiv  11983  lcmneg  16640  vdwlem12  17030  dpjidcl  20078  mplbas2  22060  monmat2matmon  22830  bwth  23418  cnextfun  24072  elbl4  24576  metucn  24584  dvradcnv  26464  dchrisum0lem2a  27561  axcontlem4  28982  cnlnadjlem2  32087  chirredlem2  32410  mdsymlem5  32426  sibfof  34342  relowlssretop  37364  matunitlindflem1  37623  poimirlem29  37656  unichnidl  38038  dmncan2  38084  cvrexchlem  39421  evlsvvval  42573  jm2.26  43014  radcnvrat  44333  binomcxplemnotnn0  44375  suplesup  45350  dvnmptdivc  45953  fourierdlem64  46185  fourierdlem74  46195  fourierdlem75  46196  fourierdlem83  46204  etransclem35  46284  iundjiun  46475  hoidmvlelem2  46611