im.bldor<

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

((phiveechi)to(psiveechi))

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
id2(chitochi)
1, 2im.bldor<>3((phiveechi)to(psiveechi))