Theorem sylanl2 693

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  mpanlr1  718  adantlrl  732  adantlrr  733  1stconst  8083  2ndconst  8084  oesuclem  8498  oelim  8507  undom  9041  mulsub  11645  divsubdiv  11922  lcmneg  16651  vdwlem12  17042  dpjidcl  20121  mplbas2  22153  evlsvvval  22204  monmat2matmon  22942  bwth  23528  cnextfun  24182  elbl4  24681  metucn  24689  dvradcnv  26542  dchrisum0lem2a  27639  axcontlem4  29226  cnlnadjlem2  32329  chirredlem2  32652  mdsymlem5  32668  sibfof  34647  fineqvnttrclselem1  35429  relowlssretop  37869  matunitlindflem1  38127  poimirlem29  38160  unichnidl  38542  dmncan2  38588  cvrexchlem  40055  jm2.26  43591  radcnvrat  44888  binomcxplemnotnn0  44930  suplesup  45913  dvnmptdivc  46510  fourierdlem64  46742  fourierdlem74  46752  fourierdlem75  46753  fourierdlem83  46761  etransclem35  46841  iundjiun  47032  hoidmvlelem2  47168