anc2<

Theorem.

Arguments:

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

Assertions:

((phito(psitochi))to(phito(psito(phiwedgechi))))

Proof:

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