Theorem sylanl2 677

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 601	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 206  df-an 396

This theorem is referenced by:  mpanlr1  702  adantlrl  716  adantlrr  717  1stconst  7911  2ndconst  7912  oesuclem  8317  oelim  8326  mulsub  11348  divsubdiv  11621  lcmneg  16236  vdwlem12  16621  dpjidcl  19576  mplbas2  21153  monmat2matmon  21881  bwth  22469  cnextfun  23123  elbl4  23625  metucn  23633  dvradcnv  25485  dchrisum0lem2a  26570  axcontlem4  27238  cnlnadjlem2  30331  chirredlem2  30654  mdsymlem5  30670  sibfof  32207  relowlssretop  35461  matunitlindflem1  35700  poimirlem29  35733  unichnidl  36116  dmncan2  36162  cvrexchlem  37360  jm2.26  40740  radcnvrat  41821  binomcxplemnotnn0  41863  suplesup  42768  dvnmptdivc  43369  fourierdlem64  43601  fourierdlem74  43611  fourierdlem75  43612  fourierdlem83  43620  etransclem35  43700  iundjiun  43888  hoidmvlelem2  44024