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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanlr1  704  adantlrl  718  adantlrr  719  1stconst  7798  2ndconst  7799  oesuclem  8153  oelim  8162  mulsub  11086  divsubdiv  11359  lcmneg  15950  vdwlem12  16331  dpjidcl  19183  mplbas2  20254  monmat2matmon  21435  bwth  22021  cnextfun  22675  elbl4  23176  metucn  23184  dvradcnv  25012  dchrisum0lem2a  26096  axcontlem4  26756  cnlnadjlem2  29848  chirredlem2  30171  mdsymlem5  30187  sibfof  31602  relowlssretop  34648  matunitlindflem1  34892  poimirlem29  34925  unichnidl  35313  dmncan2  35359  cvrexchlem  36559  jm2.26  39605  radcnvrat  40652  binomcxplemnotnn0  40694  suplesup  41613  dvnmptdivc  42229  fourierdlem64  42462  fourierdlem74  42472  fourierdlem75  42473  fourierdlem83  42481  etransclem35  42561  iundjiun  42749  hoidmvlelem2  42885