im.bldex

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

(existsxphitoexistsxpsi)

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
1ax-gen2forallx(phitopsi)
im.bldext3(forallx(phitopsi)to(existsxphitoexistsxpsi))
2, 3ax-mp4(existsxphitoexistsxpsi)