Theorem pm11.71 16354

Description: Theorem *11.71 in [WhiteheadRussell] p. 166.

Assertion

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

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

Proof of Theorem pm11.71

Step	Hyp	Ref	Expression
1		ax-17 1317	. . . . 5 |- (ph -> A.yph)
2		ax-17 1317	. . . . 5 |- (ps -> A.yps)
3	1, 2	hbim 1354	. . . 4 |- ((ph -> ps) -> A.y(ph -> ps))
4		ax-17 1317	. . . . 5 |- (ch -> A.xch)
5		ax-17 1317	. . . . 5 |- (th -> A.xth)
6	4, 5	hbim 1354	. . . 4 |- ((ch -> th) -> A.x(ch -> th))
7	3, 6	aaan 1477	. . 3 |- (A.xA.y((ph -> ps) /\ (ch -> th)) <-> (A.x(ph -> ps) /\ A.y(ch -> th)))
8		prth 615	. . . 4 |- (((ph -> ps) /\ (ch -> th)) -> ((ph /\ ch) -> (ps /\ th)))
9	8	2alimi 1339	. . 3 |- (A.xA.y((ph -> ps) /\ (ch -> th)) -> A.xA.y((ph /\ ch) -> (ps /\ th)))
10	7, 9	sylbir 218	. 2 |- ((A.x(ph -> ps) /\ A.y(ch -> th)) -> A.xA.y((ph /\ ch) -> (ps /\ th)))
11	4	hbex 1353	. . . . 5 |- (E.ych -> A.xE.ych)
12		pm3.21 306	. . . . . . 7 |- (E.ych -> (ph -> (ph /\ E.ych)))
13		simpl 346	. . . . . . . 8 |- ((ps /\ E.yth) -> ps)
14	13	imim2i 11	. . . . . . 7 |- (((ph /\ E.ych) -> (ps /\ E.yth)) -> ((ph /\ E.ych) -> ps))
15	12, 14	syl9 71	. . . . . 6 |- (E.ych -> (((ph /\ E.ych) -> (ps /\ E.yth)) -> (ph -> ps)))
16		exim 1386	. . . . . . 7 |- (A.y((ph /\ ch) -> (ps /\ th)) -> (E.y(ph /\ ch) -> E.y(ps /\ th)))
17		19.42v 1688	. . . . . . 7 |- (E.y(ph /\ ch) <-> (ph /\ E.ych))
18		19.42v 1688	. . . . . . 7 |- (E.y(ps /\ th) <-> (ps /\ E.yth))
19	16, 17, 18	3imtr3g 611	. . . . . 6 |- (A.y((ph /\ ch) -> (ps /\ th)) -> ((ph /\ E.ych) -> (ps /\ E.yth)))
20	15, 19	syl5 20	. . . . 5 |- (E.ych -> (A.y((ph /\ ch) -> (ps /\ th)) -> (ph -> ps)))
21	11, 20	alimd 1343	. . . 4 |- (E.ych -> (A.xA.y((ph /\ ch) -> (ps /\ th)) -> A.x(ph -> ps)))
22	21	adantl 424	. . 3 |- ((E.xph /\ E.ych) -> (A.xA.y((ph /\ ch) -> (ps /\ th)) -> A.x(ph -> ps)))
23	1	hbex 1353	. . . . . 6 |- (E.xph -> A.yE.xph)
24		pm3.2 305	. . . . . . . 8 |- (E.xph -> (ch -> (E.xph /\ ch)))
25		simpr 350	. . . . . . . . 9 |- ((E.xps /\ th) -> th)
26	25	imim2i 11	. . . . . . . 8 |- (((E.xph /\ ch) -> (E.xps /\ th)) -> ((E.xph /\ ch) -> th))
27	24, 26	syl9 71	. . . . . . 7 |- (E.xph -> (((E.xph /\ ch) -> (E.xps /\ th)) -> (ch -> th)))
28		exim 1386	. . . . . . . 8 |- (A.x((ph /\ ch) -> (ps /\ th)) -> (E.x(ph /\ ch) -> E.x(ps /\ th)))
29		19.41v 1685	. . . . . . . 8 |- (E.x(ph /\ ch) <-> (E.xph /\ ch))
30		19.41v 1685	. . . . . . . 8 |- (E.x(ps /\ th) <-> (E.xps /\ th))
31	28, 29, 30	3imtr3g 611	. . . . . . 7 |- (A.x((ph /\ ch) -> (ps /\ th)) -> ((E.xph /\ ch) -> (E.xps /\ th)))
32	27, 31	syl5 20	. . . . . 6 |- (E.xph -> (A.x((ph /\ ch) -> (ps /\ th)) -> (ch -> th)))
33	23, 32	alimd 1343	. . . . 5 |- (E.xph -> (A.yA.x((ph /\ ch) -> (ps /\ th)) -> A.y(ch -> th)))
34		ax-7 1304	. . . . 5 |- (A.xA.y((ph /\ ch) -> (ps /\ th)) -> A.yA.x((ph /\ ch) -> (ps /\ th)))
35	33, 34	syl5 20	. . . 4 |- (E.xph -> (A.xA.y((ph /\ ch) -> (ps /\ th)) -> A.y(ch -> th)))
36	35	adantr 425	. . 3 |- ((E.xph /\ E.ych) -> (A.xA.y((ph /\ ch) -> (ps /\ th)) -> A.y(ch -> th)))
37	22, 36	jcad 661	. 2 |- ((E.xph /\ E.ych) -> (A.xA.y((ph /\ ch) -> (ps /\ th)) -> (A.x(ph -> ps) /\ A.y(ch -> th))))
38	10, 37	impbid2 576	1 |- ((E.xph /\ E.ych) -> ((A.x(ph -> ps) /\ A.y(ch -> th)) <-> A.xA.y((ph /\ ch) -> (ps /\ th))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296  E.wex 1326

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain