anmp121

Theorem.

Arguments:

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

Hypotheses:

psi
(((phiwedge(psiwedgechi))wedgetheta)totau)

Assertions:

(((phiwedgechi)wedgetheta)totau)

Proof:

Hyp Ref Line Expr
Hypo1psi
2(((phiwedge(psiwedgechi))wedgetheta)totau)
2exp3((phiwedge(psiwedgechi))to(thetatotau))
1, 3anmp214((phiwedgechi)to(thetatotau))
4imp5(((phiwedgechi)wedgetheta)totau)