Theorem sylanl2 679

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanlr1  704  adantlrl  718  adantlrr  719  1stconst  7789  2ndconst  7790  oesuclem  8144  oelim  8153  mulsub  11077  divsubdiv  11350  lcmneg  15941  vdwlem12  16322  dpjidcl  19174  mplbas2  20245  monmat2matmon  21426  bwth  22012  cnextfun  22666  elbl4  23167  metucn  23175  dvradcnv  25003  dchrisum0lem2a  26087  axcontlem4  26747  cnlnadjlem2  29839  chirredlem2  30162  mdsymlem5  30178  sibfof  31593  relowlssretop  34638  matunitlindflem1  34882  poimirlem29  34915  unichnidl  35303  dmncan2  35349  cvrexchlem  36549  jm2.26  39592  radcnvrat  40639  binomcxplemnotnn0  40681  suplesup  41600  dvnmptdivc  42216  fourierdlem64  42449  fourierdlem74  42459  fourierdlem75  42460  fourierdlem83  42468  etransclem35  42548  iundjiun  42736  hoidmvlelem2  42872