ax10b

Theorem.

Arguments:

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

Assertions:

(forallx(xeqy)to(forallxphileftrightarrowforallyphi))

Proof:

Hyp Ref Line Expr
ax101(forallx(xeqy)to(forallxphitoforallyphi))
ax102(forally(yeqx)to(forallyphitoforallxphi))
2aleqcom3(forallx(xeqy)to(forallyphitoforallxphi))
1, 3>bid4(forallx(xeqy)to(forallxphileftrightarrowforallyphi))