rpi43
Theorem.
A syllogism rule of inference.
Description:
syl7 in set.mm
Arguments:
(pr),
(pr),
(pr),
(pr),
(pr),
Hypotheses:
(
)
(
(
(
)))
Assertions:
(
(
(
)))
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
)
2
(
(
(
)))
1
syl>
3
((
)
(
))
2, 3
rpi33
4
(
(
(
)))