bi.bldsb

Theorem.

Arguments:

(st), (sv), (pr), (pr),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ), (, ), (, ),

Hypotheses:

()

Assertions:

([/][/])

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	()
1	bi.bldan>	2	((())(()))
2	eqt-∃-i	3	((())(()))
3	bi.bldan>	4	((()(()))(()(())))
4	eqt-∃-i	5	((()(()))(()(())))
	df-sb	6	([/](()(())))
	df-sb	7	([/](()(())))
5, 6, 7	<2bitr	8	([/][/])