al.imdi
Theorem.
Arguments:
(sv),
(pr),
(pr),
Assertions:
(
(
)
(
))
Proof:
Hyp
Ref
Line
Expr
ax4
1
(
)
1
syl>
2
((
)
(
))
2
ax4
3
(
(
)
(
))
3
ax5
4
(
(
)
(
))
ax5
5
(
(
)
(
))
4, 5
syl
6
(
(
)
(
))