<and

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

(phito(psito(psiwedgephi)))

Proof:

Hyp Ref Line Expr
>and1(psito(phito(psiwedgephi)))
1com12i2(phito(psito(psiwedgephi)))