Theorem syl2ani 606

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 605	. 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏))
5	1, 4	sylani 603	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  2651  fvf1pr  7343  frxp  8167  poxp2  8184  mapen  9207  rex2dom  9309  fin1a2lem9  10477  coprmproddvdslem  16709  psss  18650  mgmidmo  18698  aannenlem1  26388  funtransport  35995  cgrxfr  36019  btwnxfr  36020  weiunpo  36431  bj-cbv3tb  36753