Theorem pm11.71 38597

Description: Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)

Assertion

Ref	Expression
pm11.71	|- ( ( E. x ph /\ E. y ch ) -> ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) <-> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) ) )

Distinct variable groups:   ph, y   ps, y   ch, x   th, x

Allowed substitution hints:   ph( x)   ps( x)   ch( y)   th( y)

Proof of Theorem pm11.71

Step	Hyp	Ref	Expression
1		nfv 1843	. . . 4 |- F/ y ( ph -> ps )
2		nfv 1843	. . . 4 |- F/ x ( ch -> th )
3	1, 2	aaan 2170	. . 3 |- ( A. x A. y ( ( ph -> ps ) /\ ( ch -> th ) ) <-> ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) )
4		prth 595	. . . 4 |- ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph /\ ch ) -> ( ps /\ th ) ) )
5	4	2alimi 1740	. . 3 |- ( A. x A. y ( ( ph -> ps ) /\ ( ch -> th ) ) -> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) )
6	3, 5	sylbir 225	. 2 |- ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) -> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) )
7		nfv 1843	. . . . . 6 |- F/ x ch
8	7	nfex 2154	. . . . 5 |- F/ x E. y ch
9		exim 1761	. . . . . . 7 |- ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( E. y ( ph /\ ch ) -> E. y ( ps /\ th ) ) )
10		19.42v 1918	. . . . . . 7 |- ( E. y ( ph /\ ch ) <-> ( ph /\ E. y ch ) )
11		19.42v 1918	. . . . . . 7 |- ( E. y ( ps /\ th ) <-> ( ps /\ E. y th ) )
12	9, 10, 11	3imtr3g 284	. . . . . 6 |- ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) )
13		pm3.21 464	. . . . . . 7 |- ( E. y ch -> ( ph -> ( ph /\ E. y ch ) ) )
14		simpl 473	. . . . . . . 8 |- ( ( ps /\ E. y th ) -> ps )
15	14	imim2i 16	. . . . . . 7 |- ( ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) -> ( ( ph /\ E. y ch ) -> ps ) )
16	13, 15	syl9 77	. . . . . 6 |- ( E. y ch -> ( ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) -> ( ph -> ps ) ) )
17	12, 16	syl5 34	. . . . 5 |- ( E. y ch -> ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ph -> ps ) ) )
18	8, 17	alimd 2081	. . . 4 |- ( E. y ch -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. x ( ph -> ps ) ) )
19	18	adantl 482	. . 3 |- ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. x ( ph -> ps ) ) )
20		ax-11 2034	. . . . 5 |- ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) )
21		nfv 1843	. . . . . . 7 |- F/ y ph
22	21	nfex 2154	. . . . . 6 |- F/ y E. x ph
23		exim 1761	. . . . . . . 8 |- ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( E. x ( ph /\ ch ) -> E. x ( ps /\ th ) ) )
24		19.41v 1914	. . . . . . . 8 |- ( E. x ( ph /\ ch ) <-> ( E. x ph /\ ch ) )
25		19.41v 1914	. . . . . . . 8 |- ( E. x ( ps /\ th ) <-> ( E. x ps /\ th ) )
26	23, 24, 25	3imtr3g 284	. . . . . . 7 |- ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) )
27		pm3.2 463	. . . . . . . 8 |- ( E. x ph -> ( ch -> ( E. x ph /\ ch ) ) )
28		simpr 477	. . . . . . . . 9 |- ( ( E. x ps /\ th ) -> th )
29	28	imim2i 16	. . . . . . . 8 |- ( ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) -> ( ( E. x ph /\ ch ) -> th ) )
30	27, 29	syl9 77	. . . . . . 7 |- ( E. x ph -> ( ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) -> ( ch -> th ) ) )
31	26, 30	syl5 34	. . . . . 6 |- ( E. x ph -> ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ch -> th ) ) )
32	22, 31	alimd 2081	. . . . 5 |- ( E. x ph -> ( A. y A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
33	20, 32	syl5 34	. . . 4 |- ( E. x ph -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
34	33	adantr 481	. . 3 |- ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
35	19, 34	jcad 555	. 2 |- ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) ) )
36	6, 35	impbid2 216	1 |- ( ( E. x ph /\ E. y ch ) -> ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) <-> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)