Theorem sylanr2 684

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 395

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 207  df-an 396

This theorem is referenced by:  adantrrl  725  adantrrr  726  unfi  9105  isfin7-2  10318  mulsub  11593  fzsubel  13514  expsub  14072  ramlb  16990  0ram  16991  ressmplvsca  22009  tgcl  22934  fgss2  23839  nmoid  24707  madebdaylemlrcut  27891  numclwwlkqhash  30445  chirredlem4  32464  pibt2  37733  lindsadd  37934  poimirlem28  37969  pridlc3  38394  stoweidlem34  46462