bi>an

Theorem.

Arguments:

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

Hypotheses:

(phito(psileftrightarrowchi))

Assertions:

((phiwedgepsi)tochi)

Proof:

Hyp Ref Line Expr
Hypo1(phito(psileftrightarrowchi))
1bi>2(phito(psitochi))
2imp3((phiwedgepsi)tochi)