19.39

Theorem.

Arguments:

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

Assertions:

((existsxphitoexistsxpsi)toexistsx(phitopsi))

Proof:

Hyp Ref Line Expr
al-ex1(forallxphitoexistsxphi)
1syl>2((existsxphitoexistsxpsi)to(forallxphitoexistsxpsi))
bexim3(existsx(phitopsi)leftrightarrow(forallxphitoexistsxpsi))
2, 3brpi22<4((existsxphitoexistsxpsi)toexistsx(phitopsi))