Theorem sylanl2 679

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mpanlr1  704  adantlrl  718  adantlrr  719  1stconst  8119  2ndconst  8120  oesuclem  8559  oelim  8568  undom  9100  mulsub  11708  divsubdiv  11985  lcmneg  16617  vdwlem12  17007  dpjidcl  20070  mplbas2  22050  monmat2matmon  22817  bwth  23405  cnextfun  24059  elbl4  24563  metucn  24571  dvradcnv  26447  dchrisum0lem2a  27543  axcontlem4  28898  cnlnadjlem2  31998  chirredlem2  32321  mdsymlem5  32337  sibfof  34205  relowlssretop  37110  matunitlindflem1  37357  poimirlem29  37390  unichnidl  37772  dmncan2  37818  cvrexchlem  39158  evlsvvval  42283  jm2.26  42727  radcnvrat  44055  binomcxplemnotnn0  44097  suplesup  45020  dvnmptdivc  45625  fourierdlem64  45857  fourierdlem74  45867  fourierdlem75  45868  fourierdlem83  45876  etransclem35  45956  iundjiun  46147  hoidmvlelem2  46283