anmp<

Theorem.

Arguments:

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

Hypotheses:

((phiwedgepsi)tochi)
phi

Assertions:

(psitochi)

Proof:

Hyp Ref Line Expr
Hypo1((phiwedgepsi)tochi)
2phi
1exp3(phito(psitochi))
2, 3ax-mp4(psitochi)