sb-bv

Theorem.

Arguments:

a (st), x (sv), phi (pr),

Dummy variables:

z (sv),

Distinct variable conditions:

(z, a), (z, x), (z, phi),

Hypotheses:

(x bound in phi)

Assertions:

([a/x]phileftrightarrowphi)

Proof:

Hyp Ref Line Expr
Hypo1(x bound in phi)
1sb-bvw2([z/x]phileftrightarrowphi)
2bi.bldsb3([a/z][z/x]phileftrightarrow[a/z]phi)
sb-bvw4([a/z]phileftrightarrowphi)
3, 4bitr5([a/z][z/x]phileftrightarrowphi)
sbco2w6([a/z][z/x]phileftrightarrow[a/x]phi)
5, 6<>bitr7([a/x]phileftrightarrowphi)