Theorem sylanl2 678

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  703  adantlrl  717  adantlrr  718  1stconst  7940  2ndconst  7941  oesuclem  8355  oelim  8364  undom  8846  mulsub  11418  divsubdiv  11691  lcmneg  16308  vdwlem12  16693  dpjidcl  19661  mplbas2  21243  monmat2matmon  21973  bwth  22561  cnextfun  23215  elbl4  23719  metucn  23727  dvradcnv  25580  dchrisum0lem2a  26665  axcontlem4  27335  cnlnadjlem2  30430  chirredlem2  30753  mdsymlem5  30769  sibfof  32307  relowlssretop  35534  matunitlindflem1  35773  poimirlem29  35806  unichnidl  36189  dmncan2  36235  cvrexchlem  37433  jm2.26  40824  radcnvrat  41932  binomcxplemnotnn0  41974  suplesup  42878  dvnmptdivc  43479  fourierdlem64  43711  fourierdlem74  43721  fourierdlem75  43722  fourierdlem83  43730  etransclem35  43810  iundjiun  43998  hoidmvlelem2  44134