bitrd

Theorem.

Arguments:

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

Hypotheses:

(phito(chileftrightarrowtheta))
(phito(psileftrightarrowchi))

Assertions:

(phito(psileftrightarrowtheta))

Proof:

Hyp Ref Line Expr
Hypo1(phito(chileftrightarrowtheta))
2(phito(psileftrightarrowchi))
2bi>3(phito(psitochi))
1bi>4(phito(chitotheta))
3, 4syld5(phito(psitotheta))
1bi<6(phito(thetatochi))
2bi<7(phito(chitopsi))
6, 7syld8(phito(thetatopsi))
5, 8>bid9(phito(psileftrightarrowtheta))