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  2645  fvf1pr  7247  frxp  8062  poxp2  8079  mapen  9061  rex2dom  9144  fin1a2lem9  10306  coprmproddvdslem  16575  psss  18488  mgmidmo  18570  aannenlem1  26264  funtransport  36096  cgrxfr  36120  btwnxfr  36121  weiunpo  36530  bj-cbv3tb  36852