Theorem syl2ani 619

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 618	. 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏))
5	1, 4	sylani 616	1 ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  2mo  2674  fvf1pr  7313  frxp  8136  poxp2  8153  mapen  9153  rex2dom  9237  fin1a2lem9  10479  coprmproddvdslem  16830  psss  18747  mgmidmo  18831  aannenlem1  26648  karddom  35812  kardsdom  35813  funtransport  36776  cgrxfr  36800  btwnxfr  36801  weiunpo  37233  bj-cbv3tb  37679