bcom12

Theorem.

Arguments:

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

Assertions:

((phito(psitochi))leftrightarrow(psito(phitochi)))

Proof:

Hyp Ref Line Expr
com121((phito(psitochi))to(psito(phitochi)))
com122((psito(phitochi))to(phito(psitochi)))
1, 2>bii3((phito(psitochi))leftrightarrow(psito(phitochi)))