anc<

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phitopsi)to(phito(phiwedgepsi)))

Proof:

Hyp Ref Line Expr
>and1(phito(psito(phiwedgepsi)))
1ax22((phitopsi)to(phito(phiwedgepsi)))