anmp<>d

Theorem.

Arguments:

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

Hypotheses:

(phitochi)
(phitopsi)
(phito((psiwedgechi)totheta))

Assertions:

(phitotheta)

Proof:

Hyp Ref Line Expr
Hypo1(phitochi)
2(phitopsi)
3(phito((psiwedgechi)totheta))
2, 3anmp<d4(phito(chitotheta))
1, 4mpd5(phitotheta)