bsylan9

Theorem.

Arguments:

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

Hypotheses:

(thetato(chileftrightarrowtau))
(phito(psileftrightarrowchi))

Assertions:

((phiwedgetheta)to(psileftrightarrowtau))

Proof:

Hyp Ref Line Expr
Hypo1(thetato(chileftrightarrowtau))
2(phito(psileftrightarrowchi))
2adan>3((phiwedgetheta)to(psileftrightarrowchi))
1adan<4((phiwedgetheta)to(chileftrightarrowtau))
3, 4bitrd5((phiwedgetheta)to(psileftrightarrowtau))