rpi33

Theorem. A syllogism rule of inference.

Description:

syl6 in set.mm

Arguments:

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

Hypotheses:

(chitotheta)
(phito(psitochi))

Assertions:

(phito(psitotheta))

Proof:

Hyp Ref Line Expr
Hypo1(chitotheta)
2(phito(psitochi))
1syl<3((psitochi)to(psitotheta))
2, 3syl4(phito(psitotheta))