Theorem sylanr1 692

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 624	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃))
3		sylanr1.2	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)
4	2, 3	sylan2 602	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  adantrll  732  adantrlr  733  sbthlem9  9061  unfi  9133  pczpre  16874  cpmadugsumlemF  22924  blsscls2  24552  rpvmasumlem  27539  leopmuli  32293  chirredlem1  32550  chirredlem3  32552  pibt2  37872  mhpind  43137  dvconstbi  44871  bccbc  44882  reccot  50340  rectan  50341  aacllem  50383