19.24

Theorem.

Arguments:

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

Assertions:

((forallxphitoforallxpsi)toexistsx(phitopsi))

Proof:

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