Theorem sylanr2 682

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  adantrrl  723  adantrrr  724  unfi  9172  isfin7-2  10391  mulsub  11657  fzsubel  13537  expsub  14076  ramlb  16952  0ram  16953  ressmplvsca  21586  tgcl  22472  fgss2  23378  nmoid  24259  madebdaylemlrcut  27393  numclwwlkqhash  29628  chirredlem4  31646  pibt2  36298  lindsadd  36481  poimirlem28  36516  pridlc3  36941  stoweidlem34  44750