eq.sub

Theorem.

Arguments:

(coll), (coll),

Dummy variables:

(sv),

Distinct variable conditions:

(, ), (, ),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df-sub	1	(()(()()))
	df-sub	2	(()(()()))
1, 2	bi.bldan<>	3	((()())((()())(()())))
	al.dfbi	4	((()())((()())(()())))
3, 4	><bitr	5	((()())(()()))
	df-equ	6	(()(()()))
5, 6	bitr	7	(()(()()))