im.bldsb

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

([y/x]phito[y/x]psi)

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
1ax-gen2forallx(phitopsi)
2im.bldsbt3([y/x]phito[y/x]psi)