eqt-∃mo-i

Theorem.

Arguments:

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

Hypotheses:

(phileftrightarrowpsi)

Assertions:

(_em1xphileftrightarrow_em1xpsi)

Proof:

Hyp Ref Line Expr
Hypo1(phileftrightarrowpsi)
eqid2(xeqx)
2bv-theor3(x bound in (xeqx))
1ax14((xeqx)to(phileftrightarrowpsi))
2, 3, 4eqt-∃mo-d5(_em1xphileftrightarrow_em1xpsi)