brpi21

Theorem.

Arguments:

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

Hypotheses:

(chileftrightarrowphi)
(phitopsi)

Assertions:

(chitopsi)

Proof:

Hyp Ref Line Expr
Hypo1(chileftrightarrowphi)
2(phitopsi)
1bi>3(chitophi)
2, 3syl4(chitopsi)