Theorem sylanl2 682

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 603	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  707  adantlrl  721  adantlrr  722  1stconst  8050  2ndconst  8051  oesuclem  8460  oelim  8469  undom  9003  mulsub  11593  divsubdiv  11871  lcmneg  16572  vdwlem12  16963  dpjidcl  20035  mplbas2  22020  evlsvvval  22071  monmat2matmon  22789  bwth  23375  cnextfun  24029  elbl4  24528  metucn  24536  dvradcnv  26386  dchrisum0lem2a  27480  axcontlem4  29036  cnlnadjlem2  32139  chirredlem2  32462  mdsymlem5  32478  sibfof  34484  fineqvnttrclselem1  35265  relowlssretop  37679  matunitlindflem1  37937  poimirlem29  37970  unichnidl  38352  dmncan2  38398  cvrexchlem  39865  jm2.26  43430  radcnvrat  44741  binomcxplemnotnn0  44783  suplesup  45769  dvnmptdivc  46366  fourierdlem64  46598  fourierdlem74  46608  fourierdlem75  46609  fourierdlem83  46617  etransclem35  46697  iundjiun  46888  hoidmvlelem2  47024