fv-and

Theorem.

Arguments:

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

Hypotheses:

(phito(chitoforallxchi))
(phito(psitoforallxpsi))

Assertions:

(phito((psiwedgechi)toforallx(psiwedgechi)))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chitoforallxchi))
2(phito(psitoforallxpsi))
1, 2im.bldan<>d3(phito((psiwedgechi)to(forallxpsiwedgeforallxchi)))
al.andi4(forallx(psiwedgechi)leftrightarrow(forallxpsiwedgeforallxchi))
3, 4brpi33<5(phito((psiwedgechi)toforallx(psiwedgechi)))