adan<<

Theorem.

Arguments:

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

Hypotheses:

((phiwedgepsi)tochi)

Assertions:

(((thetawedgephi)wedgepsi)tochi)

Proof:

Hyp Ref Line Expr
Hypo1((phiwedgepsi)tochi)
1exp2(phito(psitochi))
2adan<3((thetawedgephi)to(psitochi))
3imp4(((thetawedgephi)wedgepsi)tochi)