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  8091  2ndconst  8092  oesuclem  8506  oelim  8515  undom  9049  mulsub  11653  divsubdiv  11927  lcmneg  16657  vdwlem12  17048  dpjidcl  20126  mplbas2  22158  evlsvvval  22209  monmat2matmon  22946  bwth  23532  cnextfun  24186  elbl4  24685  metucn  24693  dvradcnv  26546  dchrisum0lem2a  27643  axcontlem4  29254  cnlnadjlem2  32357  chirredlem2  32680  mdsymlem5  32696  sibfof  34671  fineqvnttrclselem1  35453  relowlssretop  37892  matunitlindflem1  38150  poimirlem29  38183  unichnidl  38565  dmncan2  38611  cvrexchlem  40078  jm2.26  43614  radcnvrat  44909  binomcxplemnotnn0  44951  suplesup  45940  dvnmptdivc  46537  fourierdlem64  46769  fourierdlem74  46779  fourierdlem75  46780  fourierdlem83  46788  etransclem35  46868  iundjiun  47059  hoidmvlelem2  47195