praeclarum

Theorem.

Arguments:

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

Assertions:

(((phitopsi)wedge(chitotheta))to((phiwedgechi)to(psiwedgetheta)))

Proof:

Hyp Ref Line Expr
>and1(psito(thetato(psiwedgetheta)))
1syl<2(psito((chitotheta)to(chito(psiwedgetheta))))
2syl<3((phitopsi)to(phito((chitotheta)to(chito(psiwedgetheta)))))
3com23i4((phitopsi)to((chitotheta)to(phito(chito(psiwedgetheta)))))
4imp4b5(((phitopsi)wedge(chitotheta))to((phiwedgechi)to(psiwedgetheta)))