anabsi>

Theorem.

Arguments:

phi (pr), psi (pr), chi (pr),

Hypotheses:

(psito((phiwedgepsi)tochi))

Assertions:

((phiwedgepsi)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(psito((phiwedgepsi)tochi))
1adan<2((phiwedgepsi)to((phiwedgepsi)tochi))
2imabs3((phiwedgepsi)tochi)