Theorem sylanr2 680

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 617	. 2 ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜃))
3		sylanr2.2	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
4	2, 3	sylan2 593	1 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  adantrrl  721  adantrrr  722  unfi  8935  isfin7-2  10151  mulsub  11416  fzsubel  13289  expsub  13827  ramlb  16716  0ram  16717  ressmplvsca  21228  tgcl  22115  fgss2  23021  nmoid  23902  numclwwlkqhash  28733  chirredlem4  30749  madebdaylemlrcut  34073  pibt2  35582  lindsadd  35764  poimirlem28  35799  pridlc3  36225  stoweidlem34  43544