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