anasss<

Theorem.

Arguments:

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

Hypotheses:

((phiwedge(psiwedgechi))totheta)

Assertions:

(((phiwedgepsi)wedgechi)totheta)

Proof:

Hyp Ref Line Expr
Hypo1((phiwedge(psiwedgechi))totheta)
1exp322(phito(psito(chitotheta)))
2imp313(((phiwedgepsi)wedgechi)totheta)