adan<

Theorem.

Arguments:

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

Assertions:

((phitopsi)to((chiwedgephi)topsi))

Proof:

Hyp Ref Line Expr
siman>1((chiwedgephi)tophi)
1syl>2((phitopsi)to((chiwedgephi)topsi))