rpb33>>

Theorem.

Arguments:

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

Hypotheses:

(chileftrightarrowtheta)
(phito(psileftrightarrowchi))

Assertions:

(phito(psileftrightarrowtheta))

Proof:

Hyp Ref Line Expr
Hypo1(chileftrightarrowtheta)
2(phito(psileftrightarrowchi))
1ax13(phito(chileftrightarrowtheta))
2, 3bitrd4(phito(psileftrightarrowtheta))