exdistr

Theorem.

Arguments:

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

Distinct variable conditions:

(y, phi),

Assertions:

(existsxexistsy(phiwedgepsi)leftrightarrowexistsx(phiwedgeexistsypsi))

Proof:

Hyp Ref Line Expr
exan<1(existsy(phiwedgepsi)leftrightarrow(phiwedgeexistsypsi))
1eqt-∃-i2(existsxexistsy(phiwedgepsi)leftrightarrowexistsx(phiwedgeexistsypsi))