anmp11

Theorem.

Arguments:

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

Hypotheses:

(((phiwedgepsi)wedgechi)totheta)
phi

Assertions:

((psiwedgechi)totheta)

Proof:

Hyp Ref Line Expr
Hypo1(((phiwedgepsi)wedgechi)totheta)
2phi
1exp3((phiwedgepsi)to(chitotheta))
2, 3anmp<4(psito(chitotheta))
4imp5((psiwedgechi)totheta)