Theorem sylanl2 687

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanlr1  712  adantlrl  726  adantlrr  727  1stconst  8046  2ndconst  8047  oesuclem  8457  oelim  8466  undom  9000  mulsub  11591  divsubdiv  11869  lcmneg  16570  vdwlem12  16961  dpjidcl  20033  mplbas2  22025  evlsvvval  22076  monmat2matmon  22814  bwth  23400  cnextfun  24054  elbl4  24553  metucn  24561  dvradcnv  26411  dchrisum0lem2a  27505  axcontlem4  29061  cnlnadjlem2  32164  chirredlem2  32487  mdsymlem5  32503  sibfof  34531  fineqvnttrclselem1  35309  relowlssretop  37732  matunitlindflem1  37990  poimirlem29  38023  unichnidl  38405  dmncan2  38451  cvrexchlem  39918  jm2.26  43454  radcnvrat  44765  binomcxplemnotnn0  44807  suplesup  45791  dvnmptdivc  46388  fourierdlem64  46620  fourierdlem74  46630  fourierdlem75  46631  fourierdlem83  46639  etransclem35  46719  iundjiun  46910  hoidmvlelem2  47046