imp4b

Theorem.

Arguments:

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

Hypotheses:

(phito(psito(chito(thetatotau))))

Assertions:

((phiwedgepsi)to((chiwedgetheta)totau))

Proof:

Hyp Ref Line Expr
Hypo1(phito(psito(chito(thetatotau))))
1imp4a2(phito(psito((chiwedgetheta)totau)))
2imp3((phiwedgepsi)to((chiwedgetheta)totau))