Theorem sylanr1 679

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  adantrll  719  adantrlr  720  sbthlem9  8878  unfi  8955  pczpre  16548  cpmadugsumlemF  22025  blsscls2  23660  rpvmasumlem  26635  leopmuli  30495  chirredlem1  30752  chirredlem3  30754  pibt2  35588  mhpind  40283  dvconstbi  41952  bccbc  41963  reccot  46460  rectan  46461  aacllem  46505