eqt<>d

Theorem.

Arguments:

x (st), y (st), a (coll), b (coll), phi (pr),

Hypotheses:

(phito(aequivb))
(phito(xeqy))

Assertions:

(phito((xina)leftrightarrow(yinb)))

Proof:

Hyp Ref Line Expr
Hypo1(phito(aequivb))
2(phito(xeqy))
1, 2jca3(phito((xeqy)wedge(aequivb)))
3eqt<>4(phito((xina)leftrightarrow(yinb)))