syl>

Theorem.

Description:

Theorem *2.06 of PrincipiaMathematica, 1.100; imim1 in set.mm

Arguments:

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

Assertions:

((phitopsi)to((psitochi)to(phitochi)))

Proof:

Hyp Ref Line Expr
syl<1((psitochi)to((phitopsi)to(phitochi)))
1com12i2((phitopsi)to((psitochi)to(phitochi)))