rpi43

Theorem. A syllogism rule of inference.

Description:

syl7 in set.mm

Arguments:

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

Hypotheses:

(tautochi)
(phito(psito(chitotheta)))

Assertions:

(phito(psito(tautotheta)))

Proof:

Hyp Ref Line Expr
Hypo1(tautochi)
2(phito(psito(chitotheta)))
1syl>3((chitotheta)to(tautotheta))
2, 3rpi334(phito(psito(tautotheta)))