excom

Theorem.

Arguments:

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

Assertions:

(existsxexistsyphileftrightarrowexistsyexistsxphi)

Proof:

Hyp Ref Line Expr
excomim1(existsxexistsyphitoexistsyexistsxphi)
excomim2(existsyexistsxphitoexistsxexistsyphi)
1, 2>bii3(existsxexistsyphileftrightarrowexistsyexistsxphi)