sub-tr

Theorem.

Arguments:

(coll), (coll), (coll),

Dummy variables:

(sv),

Distinct variable conditions:

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

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	syl>	1	((()())((()())(()())))
1	2im.bldal	2	((()())((()())(()())))
	df-sub	3	(()(()()))
	df-sub	4	(()(()()))
2, 3, 4	<imtrg	5	((()())(()()))
	df-sub	6	(()(()()))
5, 6	brpi21	7	(()(()()))