syld

Theorem. Syllogism deduction.

Arguments:

phi (pr), psi (pr), chi (pr), theta (pr),

Hypotheses:

(phito(chitotheta))
(phito(psitochi))

Assertions:

(phito(psitotheta))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chitotheta))
2(phito(psitochi))
1syl<3(phito((psitochi)to(psitotheta)))
3ax24((phito(psitochi))to(phito(psitotheta)))
2, 4ax-mp5(phito(psitotheta))