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  9107  unfi  9179  pczpre  17018  cpmadugsumlemF  23187  blsscls2  24816  rpvmasumlem  27807  leopmuli  32728  chirredlem1  32985  chirredlem3  32987  pibt2  38320  mhpind  43602  dvconstbi  45303  bccbc  45314  reccot  50820  rectan  50821  aacllem  50908