fv-alyd

Theorem.

Arguments:

x (sv), y (sv), phi (pr), psi (pr),

Hypotheses:

(phito(psitoforallxpsi))
(y bound in phi)

Assertions:

(phito(forallypsitoforallxforallypsi))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psitoforallxpsi))
2(y bound in phi)
1, 2im.bldald3(phito(forallypsitoforallyforallxpsi))
ax74(forallyforallxpsitoforallxforallypsi)
3, 4rpi335(phito(forallypsitoforallxforallypsi))