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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpanlr1  704  adantlrl  718  adantlrr  719  1stconst  8088  2ndconst  8089  oesuclem  8527  oelim  8536  undom  9061  mulsub  11659  divsubdiv  11932  lcmneg  16542  vdwlem12  16927  dpjidcl  19930  mplbas2  21603  monmat2matmon  22333  bwth  22921  cnextfun  23575  elbl4  24079  metucn  24087  dvradcnv  25940  dchrisum0lem2a  27027  axcontlem4  28263  cnlnadjlem2  31359  chirredlem2  31682  mdsymlem5  31698  sibfof  33408  relowlssretop  36330  matunitlindflem1  36570  poimirlem29  36603  unichnidl  36985  dmncan2  37031  cvrexchlem  38376  evlsvvval  41217  jm2.26  41823  radcnvrat  43155  binomcxplemnotnn0  43197  suplesup  44128  dvnmptdivc  44733  fourierdlem64  44965  fourierdlem74  44975  fourierdlem75  44976  fourierdlem83  44984  etransclem35  45064  iundjiun  45255  hoidmvlelem2  45391