eqt-∀

Theorem.

Arguments:

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

Assertions:

(forallx(phileftrightarrowpsi)to(forallxphileftrightarrowforallxpsi))

Proof:

Hyp Ref Line Expr
bi>1((phileftrightarrowpsi)to(phitopsi))
bi<2((phileftrightarrowpsi)to(psitophi))
12im.bldal3(forallx(phileftrightarrowpsi)to(forallxphitoforallxpsi))
22im.bldal4(forallx(phileftrightarrowpsi)to(forallxpsitoforallxphi))
3, 4>bid5(forallx(phileftrightarrowpsi)to(forallxphileftrightarrowforallxpsi))