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  9165  isfin7-2  10398  mulsub  11681  fzsubel  13615  expsub  14174  ramlb  17111  0ram  17112  cmprmidlmcl  21538  ressmplvsca  22246  tgcl  23194  fgss2  24100  nmoid  24968  madebdaylemlrcut  28164  numclwwlkqhash  30855  chirredlem4  32874  pibt2  38171  lindsadd  38367  poimirlem28  38397  pridlc3  38823  stoweidlem34  46862