im.bldal

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

(forallxphitoforallxpsi)

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
1ax42(forallxphitopsi)
2ax53(forallxphitoforallxpsi)