Theorem sylanl2 682

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpanlr1  707  adantlrl  721  adantlrr  722  1stconst  8052  2ndconst  8053  oesuclem  8462  oelim  8471  undom  9005  mulsub  11592  divsubdiv  11869  lcmneg  16542  vdwlem12  16932  dpjidcl  20001  mplbas2  22009  evlsvvval  22060  monmat2matmon  22780  bwth  23366  cnextfun  24020  elbl4  24519  metucn  24527  dvradcnv  26398  dchrisum0lem2a  27496  axcontlem4  29052  cnlnadjlem2  32155  chirredlem2  32478  mdsymlem5  32494  sibfof  34517  fineqvnttrclselem1  35296  relowlssretop  37612  matunitlindflem1  37861  poimirlem29  37894  unichnidl  38276  dmncan2  38322  cvrexchlem  39789  jm2.26  43353  radcnvrat  44664  binomcxplemnotnn0  44706  suplesup  45692  dvnmptdivc  46290  fourierdlem64  46522  fourierdlem74  46532  fourierdlem75  46533  fourierdlem83  46541  etransclem35  46621  iundjiun  46812  hoidmvlelem2  46948