Theorem sylanl2 681

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 602	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  706  adantlrl  720  adantlrr  721  1stconst  8042  2ndconst  8043  oesuclem  8452  oelim  8461  undom  8993  mulsub  11580  divsubdiv  11857  lcmneg  16530  vdwlem12  16920  dpjidcl  19989  mplbas2  21997  evlsvvval  22048  monmat2matmon  22768  bwth  23354  cnextfun  24008  elbl4  24507  metucn  24515  dvradcnv  26386  dchrisum0lem2a  27484  axcontlem4  29040  cnlnadjlem2  32143  chirredlem2  32466  mdsymlem5  32482  sibfof  34497  fineqvnttrclselem1  35277  relowlssretop  37564  matunitlindflem1  37813  poimirlem29  37846  unichnidl  38228  dmncan2  38274  cvrexchlem  39675  jm2.26  43240  radcnvrat  44551  binomcxplemnotnn0  44593  suplesup  45580  dvnmptdivc  46178  fourierdlem64  46410  fourierdlem74  46420  fourierdlem75  46421  fourierdlem83  46429  etransclem35  46509  iundjiun  46700  hoidmvlelem2  46836