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  9179  isfin7-2  10467  mulsub  11752  fzsubel  13687  expsub  14246  ramlb  17190  0ram  17191  cmprmidlmcl  21624  ressmplvsca  22332  tgcl  23280  fgss2  24186  nmoid  25054  madebdaylemlrcut  28278  numclwwlkqhash  30969  chirredlem4  32988  pibt2  38320  lindsadd  38516  poimirlem28  38546  pridlc3  38987  stoweidlem34  47013