Theorem sylanl2 680

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  7800  2ndconst  7801  oesuclem  8160  oelim  8169  mulsub  11121  divsubdiv  11394  lcmneg  15999  vdwlem12  16383  dpjidcl  19248  mplbas2  20802  monmat2matmon  21524  bwth  22110  cnextfun  22764  elbl4  23265  metucn  23273  dvradcnv  25115  dchrisum0lem2a  26200  axcontlem4  26860  cnlnadjlem2  29950  chirredlem2  30273  mdsymlem5  30289  sibfof  31826  relowlssretop  35060  matunitlindflem1  35333  poimirlem29  35366  unichnidl  35749  dmncan2  35795  cvrexchlem  36995  jm2.26  40316  radcnvrat  41391  binomcxplemnotnn0  41433  suplesup  42339  dvnmptdivc  42946  fourierdlem64  43178  fourierdlem74  43188  fourierdlem75  43189  fourierdlem83  43197  etransclem35  43277  iundjiun  43465  hoidmvlelem2  43601