eqt-sbi

Theorem.

Arguments:

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

Assertions:

((xeqy)to([x/z]phito[y/z]phi))

Proof:

Hyp Ref Line Expr
eqt-sb1((xeqy)to([x/z]phileftrightarrow[y/z]phi))
1bi>2((xeqy)to([x/z]phito[y/z]phi))