anmp>

Theorem.

Arguments:

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

Hypotheses:

((phiwedgepsi)tochi)
psi

Assertions:

(phitochi)

Proof:

Hyp Ref Line Expr
Hypo1((phiwedgepsi)tochi)
2psi
1exp3(phito(psitochi))
3com12i4(psito(phitochi))
2, 4ax-mp5(phitochi)