ad2an>>

Theorem.

Arguments:

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

Hypotheses:

(phitopsi)

Assertions:

((chiwedge(thetawedgephi))topsi)

Proof:

Hyp Ref Line Expr
Hypo1(phitopsi)
1adan<2((thetawedgephi)topsi)
2adan<3((chiwedge(thetawedgephi))topsi)