eqvini-sv

Theorem.

Arguments:

(sv), (sv), (sv),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	ax9-sv	1	()
	eqid	2	()
2	jct<	3	(()(()()))
3	im.bldex	4	(()(()()))
1, 4	ax-mp	5	(()())
	bv-∀b	6	( bound in ())
	ax8	7	(()(()()))
7	ax4	8	(()(()()))
8	im.bldan<d	9	(()((()())(()())))
6, 9	im.bldexd	10	(()((()())(()())))
5, 10	mpi	11	(()(()()))
	ax9-sv	12	()
	eqcomi	13	(()())
2, 13	jcti>	14	(()(()()))
14	im.bldex	15	(()(()()))
12, 15	ax-mp	16	(()())
	bv-∀b	17	( bound in ())
	ax1	18	(()(()()))
18	ax4	19	(()(()()))
19	im.bldan>d	20	(()((()())(()())))
17, 20	im.bldexd	21	(()((()())(()())))
16, 21	mpi	22	(()(()()))
11, 22	jaoi	23	((()())(()()))
23	ax1	24	((()())(()(()())))
	nor.an	25	((()())(()()))
	fv-nalx	26	( bound in ())
	fv-nalx	27	( bound in ())
26, 27	bv-∧	28	( bound in (()()))
	ax12	29	(()(()(()())))
29	imp	30	((()())(()()))
	ax8	31	(()(()()))
31	anc2<	32	(()(()(()())))
32	eqcomi	33	(()(()(()())))
28, 30, 33	ax4c1	34	((()())(()(()())))
25	bi>	35	((()())(()()))
34, 35	syl	36	((()())(()(()())))
24, 36	casei	37	(()(()()))