im.bldan<

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

((phiwedgechi)to(psiwedgechi))

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
id2(chitochi)
1, 2im.bldan<>3((phiwedgechi)to(psiwedgechi))