mpclosedan

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiwedge(phitopsi))topsi)

Proof:

Hyp Ref Line Expr
mpclosed1(phito((phitopsi)topsi))
1imp2((phiwedge(phitopsi))topsi)