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	anim2i 591	. 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3		sylanl2.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 487	1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpanlr1  718  adantlrl  752  adantlrr  753  oesuclem  7492  oelim  7501  mulsub  10352  divsubdiv  10620  lcmneg  15154  vdwlem12  15534  dpjidcl  18280  mplbas2  19291  monmat2matmon  20448  bwth  21023  cnextfun  21678  elbl4  22178  metucn  22186  dvradcnv  23979  dchrisum0lem2a  25006  axcontlem4  25647  cnlnadjlem2  28311  chirredlem2  28634  mdsymlem5  28650  sibfof  29729  relowlssretop  32387  matunitlindflem1  32575  poimirlem29  32608  unichnidl  33000  dmncan2  33046  cvrexchlem  33723  jm2.26  36587  radcnvrat  37535  binomcxplemnotnn0  37577  suplesup  38496  dvnmptdivc  38828  fourierdlem64  39063  fourierdlem74  39073  fourierdlem75  39074  fourierdlem83  39082  etransclem35  39162  iundjiun  39353  hoidmvlelem2  39486