Theorem sylanr2 696

Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Hypotheses

Ref	Expression
sylanr2.1	⊢ (𝜑 → 𝜃)
sylanr2.2	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
sylanr2	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏)

Proof of Theorem sylanr2

Step	Hyp	Ref	Expression
1		sylanr2.1	. . 3 ⊢ (𝜑 → 𝜃)
2	1	anim2i 629	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜃))
3		sylanr2.2	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
4	2, 3	sylan2 605	1 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  adantrrl  737  adantrrr  738  unfi  9158  isfin7-2  10391  mulsub  11668  fzsubel  13601  expsub  14160  ramlb  17097  0ram  17098  cmprmidlmcl  21505  ressmplvsca  22211  tgcl  23156  fgss2  24062  nmoid  24930  madebdaylemlrcut  28123  numclwwlkqhash  30773  chirredlem4  32792  pibt2  38096  lindsadd  38297  poimirlem28  38332  pridlc3  38757  stoweidlem34  46781