eqt-∃-i

Theorem.

Arguments:

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

Hypotheses:

(phileftrightarrowpsi)

Assertions:

(existsxphileftrightarrowexistsxpsi)

Proof:

Hyp Ref Line Expr
Hypo1(phileftrightarrowpsi)
1ax-gen2forallx(phileftrightarrowpsi)
eqt-∃3(forallx(phileftrightarrowpsi)to(existsxphileftrightarrowexistsxpsi))
2, 3ax-mp4(existsxphileftrightarrowexistsxpsi)