anc>

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phitopsi)to(phito(psiwedgephi)))

Proof:

Hyp Ref Line Expr
<and1(phito(psito(psiwedgephi)))
1ax22((phitopsi)to(phito(psiwedgephi)))