Theorem sylanl2 680

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpanlr1  705  adantlrl  719  adantlrr  720  1stconst  8086  2ndconst  8087  oesuclem  8525  oelim  8534  undom  9059  mulsub  11657  divsubdiv  11930  lcmneg  16540  vdwlem12  16925  dpjidcl  19928  mplbas2  21597  monmat2matmon  22326  bwth  22914  cnextfun  23568  elbl4  24072  metucn  24080  dvradcnv  25933  dchrisum0lem2a  27020  axcontlem4  28225  cnlnadjlem2  31321  chirredlem2  31644  mdsymlem5  31660  sibfof  33339  relowlssretop  36244  matunitlindflem1  36484  poimirlem29  36517  unichnidl  36899  dmncan2  36945  cvrexchlem  38290  evlsvvval  41135  jm2.26  41741  radcnvrat  43073  binomcxplemnotnn0  43115  suplesup  44049  dvnmptdivc  44654  fourierdlem64  44886  fourierdlem74  44896  fourierdlem75  44897  fourierdlem83  44905  etransclem35  44985  iundjiun  45176  hoidmvlelem2  45312