Theorem syl2ani 608

Description: A syllogism inference. (Contributed by NM, 3-Aug-1999.)

Hypotheses

Ref	Expression
syl2ani.1	⊢ (𝜑 → 𝜒)
syl2ani.2	⊢ (𝜂 → 𝜃)
syl2ani.3	⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
syl2ani	⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏))

Proof of Theorem syl2ani

Step	Hyp	Ref	Expression
1		syl2ani.1	. 2 ⊢ (𝜑 → 𝜒)
2		syl2ani.2	. . 3 ⊢ (𝜂 → 𝜃)
3		syl2ani.3	. . 3 ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))
4	2, 3	sylan2i 607	. 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏))
5	1, 4	sylani 605	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:  2mo  2649  fvf1pr  7255  frxp  8070  poxp2  8087  mapen  9073  rex2dom  9157  fin1a2lem9  10322  coprmproddvdslem  16593  psss  18507  mgmidmo  18589  aannenlem1  26296  funtransport  36206  cgrxfr  36230  btwnxfr  36231  weiunpo  36640  bj-cbv3tb  36963