Theorem sylanr1 695

Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Hypotheses

Ref	Expression
sylanr1.1	⊢ (𝜑 → 𝜒)
sylanr1.2	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
sylanr1	⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏)

Proof of Theorem sylanr1

Step	Hyp	Ref	Expression
1		sylanr1.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	anim1i 627	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))
3		sylanr1.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:  adantrll  735  adantrlr  736  sbthlem9  9093  unfi  9165  pczpre  16939  cpmadugsumlemF  23101  blsscls2  24730  rpvmasumlem  27723  leopmuli  32614  chirredlem1  32871  chirredlem3  32873  pibt2  38171  mhpind  43440  dvconstbi  45158  bccbc  45169  reccot  50684  rectan  50685  aacllem  50772