Theorem sylanl2 694

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanlr1  719  adantlrl  733  adantlrr  734  1stconst  8138  2ndconst  8139  oesuclem  8561  oelim  8570  undom  9112  mulsub  11786  divsubdiv  12060  lcmneg  16807  vdwlem12  17199  dpjidcl  20304  mplbas2  22381  evlsvvval  22432  matunitlindflem1  23024  monmat2matmon  23172  bwth  23758  cnextfun  24413  elbl4  24912  metucn  24920  dvradcnv  26778  dchrisum0lem2a  27874  axcontlem4  29575  cnlnadjlem2  32700  chirredlem2  33023  mdsymlem5  33039  sibfof  35042  fineqvnttrclselem1  35889  relowlssretop  38478  poimirlem29  38759  unichnidl  39157  dmncan2  39203  cvrexchlem  40668  jm2.26  44202  radcnvrat  45490  binomcxplemnotnn0  45532  suplesup  46556  dvnmptdivc  47153  fourierdlem64  47385  fourierdlem74  47395  fourierdlem75  47396  fourierdlem83  47404  etransclem35  47484  iundjiun  47675  hoidmvlelem2  47811  idomcanr  49650