exdistr
Theorem.
Arguments:
(sv),
(sv),
(pr),
(pr),
Distinct variable conditions:
(
,
),
Assertions:
(
(
)
(
))
Proof:
Hyp
Ref
Line
Expr
exan<
1
(
(
)
(
))
1
eqt-∃-i
2
(
(
)
(
))