al-ex

Theorem.

Arguments:

x (sv), phi (pr),

Assertions:

(forallxphitoexistsxphi)

Proof:

Hyp Ref Line Expr
ax41(forallxphitophi)
spec-ex2(phitoexistsxphi)
1, 2syl3(forallxphitoexistsxphi)