brpi32

Theorem.

Arguments:

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

Hypotheses:

(thetaleftrightarrowpsi)
(phito(psitochi))

Assertions:

(phito(thetatochi))

Proof:

Hyp Ref Line Expr
Hypo1(thetaleftrightarrowpsi)
2(phito(psitochi))
1bi>3(thetatopsi)
2, 3rpi324(phito(thetatochi))