Theorem syl2ani 607

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 606	. 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏))
5	1, 4	sylani 604	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  2641  fvf1pr  7282  frxp  8105  poxp2  8122  mapen  9105  rex2dom  9193  fin1a2lem9  10361  coprmproddvdslem  16632  psss  18539  mgmidmo  18587  aannenlem1  26236  funtransport  36019  cgrxfr  36043  btwnxfr  36044  weiunpo  36453  bj-cbv3tb  36775