2im.bldal

Theorem.

Arguments:

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

Hypotheses:

(phito(psitochi))

Assertions:

(forallxphito(forallxpsitoforallxchi))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psitochi))
1im.bldal2(forallxphitoforallx(psitochi))
al.imdi3(forallx(psitochi)to(forallxpsitoforallxchi))
2, 3syl4(forallxphito(forallxpsitoforallxchi))