Theorem amosym1

Description: A symmetry with E* .

See negsym1 for more information. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	amosym1	|- ( E* x E* x F. -> E* x ph )

Proof

Step	Hyp	Ref	Expression
1		moeu	|- ( E* x E* x F. <-> ( E. x E* x F. -> E! x E* x F. ) )
2		mofal	|- E* x F.
3		19.8a	|- ( E* x F. -> E. x E* x F. )
4	3	notnotd	|- ( E* x F. -> -. -. E. x E* x F. )
5	2 4	ax-mp	|- -. -. E. x E* x F.
6	5	pm2.21i	|- ( -. E. x E* x F. -> E* x ph )
7	2	notnoti	|- -. -. E* x F.
8	7	nex	|- -. E. x -. E* x F.
9		eunex	|- ( E! x E* x F. -> E. x -. E* x F. )
10	8 9	mto	|- -. E! x E* x F.
11	10	pm2.21i	|- ( E! x E* x F. -> E* x ph )
12	6 11	ja	|- ( ( E. x E* x F. -> E! x E* x F. ) -> E* x ph )
13	1 12	sylbi	|- ( E* x E* x F. -> E* x ph )