im.bldan>d

Theorem.

Arguments:

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

Hypotheses:

(phito(psitochi))

Assertions:

(phito((thetawedgepsi)to(thetawedgechi)))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psitochi))
idd2(phito(thetatotheta))
1, 2im.bldan<>d3(phito((thetawedgepsi)to(thetawedgechi)))