>andc

Theorem.

Arguments:

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

Assertions:

((phitopsi)to((phitochi)to(phito(psiwedgechi))))

Proof:

Hyp Ref Line Expr
>and1(psito(chito(psiwedgechi)))
1syl<2((phitopsi)to(phito(chito(psiwedgechi))))
2ax23((phitopsi)to((phitochi)to(phito(psiwedgechi))))