anc2>

Theorem.

Arguments:

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

Assertions:

((phito(psitochi))to(phito(psito(chiwedgephi))))

Proof:

Hyp Ref Line Expr
<and1(phito(chito(chiwedgephi)))
1syl<2(phito((psitochi)to(psito(chiwedgephi))))
2ax23((phito(psitochi))to(phito(psito(chiwedgephi))))