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  9224  isfin7-2  10513  mulsub  11798  fzsubel  13734  expsub  14293  ramlb  17241  0ram  17242  cmprmidlmcl  21682  ressmplvsca  22394  tgcl  23342  fgss2  24248  nmoid  25116  madebdaylemlrcut  28342  numclwwlkqhash  31033  chirredlem4  33052  pibt2  38608  lindsadd  38804  poimirlem28  38834  pridlc3  39273  stoweidlem34  47317