bv-theor

Theorem.

Arguments:

x (sv), phi (pr),

Hypotheses:

phi

Assertions:

(x bound in phi)

Proof:

Hyp Ref Line Expr
Hypo1phi
1fv-theor2(phitoforallxphi)
2df-Bvp3(x bound in phi)