ex.andi

Theorem.

Arguments:

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

Assertions:

(existsx(phiwedgepsi)to(existsxphiwedgeexistsxpsi))

Proof:

Hyp Ref Line Expr
siman<1((phiwedgepsi)tophi)
1im.bldex2(existsx(phiwedgepsi)toexistsxphi)
siman>3((phiwedgepsi)topsi)
3im.bldex4(existsx(phiwedgepsi)toexistsxpsi)
2, 4jca5(existsx(phiwedgepsi)to(existsxphiwedgeexistsxpsi))