fv-alx

Theorem.

Arguments:

x (sv), phi (pr),

Assertions:

(forallxphitoforallxforallxphi)

Proof:

Hyp Ref Line Expr
id1(forallxphitoforallxphi)
1ax52(forallxphitoforallxforallxphi)