im.bldan>

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

((chiwedgephi)to(chiwedgepsi))

Proof:

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