Theorem axc5c4c711

Description: Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen as the inference rule. This proof extends the idea of axc5c711 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011)

	Ref	Expression
Assertion	axc5c4c711	|- ( ( A. x A. y -. A. x A. y ( A. y ph -> ps ) -> ( ph -> A. y ( A. y ph -> ps ) ) ) -> ( A. y ph -> A. y ps ) )

Proof

Step	Hyp	Ref	Expression
1		axc4	|- ( A. y ( A. y ph -> ps ) -> ( A. y ph -> A. y ps ) )
2		hbn1	|- ( -. A. y ( A. y ph -> ps ) -> A. y -. A. y ( A. y ph -> ps ) )
3		axc7	|- ( -. A. x -. A. x A. y ( A. y ph -> ps ) -> A. y ( A. y ph -> ps ) )
4	3	con1i	|- ( -. A. y ( A. y ph -> ps ) -> A. x -. A. x A. y ( A. y ph -> ps ) )
5	2 4	alrimih	|- ( -. A. y ( A. y ph -> ps ) -> A. y A. x -. A. x A. y ( A. y ph -> ps ) )
6		ax-11	|- ( A. y A. x -. A. x A. y ( A. y ph -> ps ) -> A. x A. y -. A. x A. y ( A. y ph -> ps ) )
7	5 6	syl	|- ( -. A. y ( A. y ph -> ps ) -> A. x A. y -. A. x A. y ( A. y ph -> ps ) )
8	1 7	nsyl4	|- ( -. A. x A. y -. A. x A. y ( A. y ph -> ps ) -> ( A. y ph -> A. y ps ) )
9		pm2.21	|- ( -. ph -> ( ph -> A. y ps ) )
10	9	spsd	|- ( -. ph -> ( A. y ph -> A. y ps ) )
11	10 1	ja	|- ( ( ph -> A. y ( A. y ph -> ps ) ) -> ( A. y ph -> A. y ps ) )
12	8 11	ja	|- ( ( A. x A. y -. A. x A. y ( A. y ph -> ps ) -> ( ph -> A. y ( A. y ph -> ps ) ) ) -> ( A. y ph -> A. y ps ) )