sb-neg

Theorem.

Arguments:

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

Dummy variables:

y (sv),

Distinct variable conditions:

(y, a), (y, x), (y, phi),

Assertions:

([a/x]lnotphileftrightarrowlnot[a/x]phi)

Proof:

Hyp Ref Line Expr
sbco2w1([a/y][y/x]lnotphileftrightarrow[a/x]lnotphi)
sbco2w2([a/y][y/x]phileftrightarrow[a/x]phi)
2bi.bldneg3(lnot[a/y][y/x]phileftrightarrowlnot[a/x]phi)
sb-negw4([y/x]lnotphileftrightarrowlnot[y/x]phi)
4bi.bldsb5([a/y][y/x]lnotphileftrightarrow[a/y]lnot[y/x]phi)
sb-negw6([a/y]lnot[y/x]phileftrightarrowlnot[a/y][y/x]phi)
1, 5<>bitr7([a/x]lnotphileftrightarrow[a/y]lnot[y/x]phi)
3, 6, 72bitr8([a/x]lnotphileftrightarrowlnot[a/x]phi)