im.bldan<>d

Theorem.

Arguments:

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

Hypotheses:

(phito(thetatotau))
(phito(psitochi))

Assertions:

(phito((psiwedgetheta)to(chiwedgetau)))

Proof:

Hyp Ref Line Expr
Hypo1(phito(thetatotau))
2(phito(psitochi))
praeclarum3(((psitochi)wedge(thetatotau))to((psiwedgetheta)to(chiwedgetau)))
1, 2jca4(phito((psitochi)wedge(thetatotau)))
3, 4syl5(phito((psiwedgetheta)to(chiwedgetau)))