sb-or

Theorem.

Arguments:

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

Dummy variables:

y (sv),

Distinct variable conditions:

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

Assertions:

([a/x](phiveepsi)leftrightarrow([a/x]phivee[a/x]psi))

Proof:

Hyp Ref Line Expr
sb-orw1([y/x](phiveepsi)leftrightarrow([y/x]phivee[y/x]psi))
1bi.bldsb2([a/y][y/x](phiveepsi)leftrightarrow[a/y]([y/x]phivee[y/x]psi))
sb-orw3([a/y]([y/x]phivee[y/x]psi)leftrightarrow([a/y][y/x]phivee[a/y][y/x]psi))
2, 3bitr4([a/y][y/x](phiveepsi)leftrightarrow([a/y][y/x]phivee[a/y][y/x]psi))
sbco2w5([a/y][y/x](phiveepsi)leftrightarrow[a/x](phiveepsi))
sbco2w6([a/y][y/x]phileftrightarrow[a/x]phi)
sbco2w7([a/y][y/x]psileftrightarrow[a/x]psi)
6, 7bi.bldor<>8(([a/y][y/x]phivee[a/y][y/x]psi)leftrightarrow([a/x]phivee[a/x]psi))
4, 5, 8>2bitr9([a/x](phiveepsi)leftrightarrow([a/x]phivee[a/x]psi))