exalswap
Theorem.
Arguments:
(sv),
(sv),
(pr),
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
fv-alx
1
(
)
1
fv-exy
2
(
)
ax4
3
(
)
3
im.bldex
4
(
)
4
im.bldal
5
(
)
2, 5
syl
6
(
)
(sv), 
(sv), 
(pr), (sv), (sv), (pr), 
)))))))