fv-aly

Theorem.

Arguments:

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

Hypotheses:

(phitoforallxphi)

Assertions:

(forallyphitoforallxforallyphi)

Proof:

Hyp Ref Line Expr
Hypo1(phitoforallxphi)
1im.bldal2(forallyphitoforallyforallxphi)
ax73(forallyforallxphitoforallxforallyphi)
2, 3syl4(forallyphitoforallxforallyphi)