Theorem sbcom 1632

Description: A commutativity law for substitution.

Assertion

Ref	Expression
sbcom	|- ([y / z][y / x]ph <-> [y / x][y / z]ph)

Proof of Theorem sbcom

Step	Hyp	Ref	Expression
1		drsb1 1539	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / z][y / x]ph))
2		hbae 1505	. . . . . . 7 |- (A.x x = z -> A.xA.x x = z)
3		drsb1 1539	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
4	2, 3	sbbid 1617	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / x][y / z]ph))
5	1, 4	bitr3d 589	. . . . 5 |- (A.x x = z -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
6	5	adantr 425	. . . 4 |- ((A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
7		hbnae 1507	. . . . . . . . 9 |- (-. A.x x = z -> A.z -. A.x x = z)
8		hbnae 1507	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
9	7, 8	hban 1356	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> A.z(-. A.x x = z /\ -. A.x x = y))
10		hbnae 1507	. . . . . . . . . 10 |- (-. A.x x = z -> A.x -. A.x x = z)
11		hbnae 1507	. . . . . . . . . 10 |- (-. A.x x = y -> A.x -. A.x x = y)
12	10, 11	hban 1356	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.x x = y) -> A.x(-. A.x x = z /\ -. A.x x = y))
13		ax-12 1310	. . . . . . . . . . 11 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
14	13	imp 377	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.x x = y) -> (z = y -> A.x z = y))
15	14	alimi 1338	. . . . . . . . 9 |- (A.x(-. A.x x = z /\ -. A.x x = y) -> A.x(z = y -> A.x z = y))
16		19.21t 1473	. . . . . . . . 9 |- (A.x(z = y -> A.x z = y) -> (A.x(z = y -> (x = y -> ph)) <-> (z = y -> A.x(x = y -> ph))))
17	12, 15, 16	3syl 24	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (A.x(z = y -> (x = y -> ph)) <-> (z = y -> A.x(x = y -> ph))))
18	9, 17	albid 1459	. . . . . . 7 |- ((-. A.x x = z /\ -. A.x x = y) -> (A.zA.x(z = y -> (x = y -> ph)) <-> A.z(z = y -> A.x(x = y -> ph))))
19	18	adantrr 431	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> (A.zA.x(z = y -> (x = y -> ph)) <-> A.z(z = y -> A.x(x = y -> ph))))
20		hbnae 1507	. . . . . . . . . 10 |- (-. A.z z = y -> A.x -. A.z z = y)
21	10, 20	hban 1356	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.z z = y) -> A.x(-. A.x x = z /\ -. A.z z = y))
22		hbnae 1507	. . . . . . . . . . . 12 |- (-. A.z z = y -> A.z -. A.z z = y)
23	7, 22	hban 1356	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.z z = y) -> A.z(-. A.x x = z /\ -. A.z z = y))
24		ax-12 1310	. . . . . . . . . . . . . 14 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
25	24	nalequcoms 1504	. . . . . . . . . . . . 13 |- (-. A.x x = z -> (-. A.z z = y -> (x = y -> A.z x = y)))
26	25	imp 377	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ -. A.z z = y) -> (x = y -> A.z x = y))
27	26	alimi 1338	. . . . . . . . . . 11 |- (A.z(-. A.x x = z /\ -. A.z z = y) -> A.z(x = y -> A.z x = y))
28		19.21t 1473	. . . . . . . . . . 11 |- (A.z(x = y -> A.z x = y) -> (A.z(x = y -> (z = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
29	23, 27, 28	3syl 24	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.z(x = y -> (z = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
30		bi2.04 177	. . . . . . . . . . 11 |- ((z = y -> (x = y -> ph)) <-> (x = y -> (z = y -> ph)))
31	30	albii 1346	. . . . . . . . . 10 |- (A.z(z = y -> (x = y -> ph)) <-> A.z(x = y -> (z = y -> ph)))
32	29, 31	syl5bb 591	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.z(z = y -> (x = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
33	21, 32	albid 1459	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.xA.z(z = y -> (x = y -> ph)) <-> A.x(x = y -> A.z(z = y -> ph))))
34		alcom 1379	. . . . . . . 8 |- (A.zA.x(z = y -> (x = y -> ph)) <-> A.xA.z(z = y -> (x = y -> ph)))
35	33, 34	syl5bb 591	. . . . . . 7 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.zA.x(z = y -> (x = y -> ph)) <-> A.x(x = y -> A.z(z = y -> ph))))
36	35	adantrl 430	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> (A.zA.x(z = y -> (x = y -> ph)) <-> A.x(x = y -> A.z(z = y -> ph))))
37	19, 36	bitr3d 589	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> (A.z(z = y -> A.x(x = y -> ph)) <-> A.x(x = y -> A.z(z = y -> ph))))
38		sb4b 1594	. . . . . . 7 |- (-. A.z z = y -> ([y / z][y / x]ph <-> A.z(z = y -> [y / x]ph)))
39		sb4b 1594	. . . . . . . . 9 |- (-. A.x x = y -> ([y / x]ph <-> A.x(x = y -> ph)))
40	39	imbi2d 674	. . . . . . . 8 |- (-. A.x x = y -> ((z = y -> [y / x]ph) <-> (z = y -> A.x(x = y -> ph))))
41	8, 40	albid 1459	. . . . . . 7 |- (-. A.x x = y -> (A.z(z = y -> [y / x]ph) <-> A.z(z = y -> A.x(x = y -> ph))))
42	38, 41	sylan9bbr 600	. . . . . 6 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> A.z(z = y -> A.x(x = y -> ph))))
43	42	adantl 424	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> A.z(z = y -> A.x(x = y -> ph))))
44		sb4b 1594	. . . . . . 7 |- (-. A.x x = y -> ([y / x][y / z]ph <-> A.x(x = y -> [y / z]ph)))
45		sb4b 1594	. . . . . . . . 9 |- (-. A.z z = y -> ([y / z]ph <-> A.z(z = y -> ph)))
46	45	imbi2d 674	. . . . . . . 8 |- (-. A.z z = y -> ((x = y -> [y / z]ph) <-> (x = y -> A.z(z = y -> ph))))
47	20, 46	albid 1459	. . . . . . 7 |- (-. A.z z = y -> (A.x(x = y -> [y / z]ph) <-> A.x(x = y -> A.z(z = y -> ph))))
48	44, 47	sylan9bb 599	. . . . . 6 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / x][y / z]ph <-> A.x(x = y -> A.z(z = y -> ph))))
49	48	adantl 424	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / x][y / z]ph <-> A.x(x = y -> A.z(z = y -> ph))))
50	37, 43, 49	3bitr4d 609	. . . 4 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
51	6, 50	pm2.61ian 534	. . 3 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
52	51	ex 402	. 2 |- (-. A.x x = y -> (-. A.z z = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph)))
53		hbae 1505	. . . 4 |- (A.x x = y -> A.zA.x x = y)
54		sbequ12 1545	. . . . 5 |- (x = y -> (ph <-> [y / x]ph))
55	54	a4s 1330	. . . 4 |- (A.x x = y -> (ph <-> [y / x]ph))
56	53, 55	sbbid 1617	. . 3 |- (A.x x = y -> ([y / z]ph <-> [y / z][y / x]ph))
57		sbequ12 1545	. . . 4 |- (x = y -> ([y / z]ph <-> [y / x][y / z]ph))
58	57	a4s 1330	. . 3 |- (A.x x = y -> ([y / z]ph <-> [y / x][y / z]ph))
59	56, 58	bitr3d 589	. 2 |- (A.x x = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
60		sbequ12 1545	. . . 4 |- (z = y -> ([y / x]ph <-> [y / z][y / x]ph))
61	60	a4s 1330	. . 3 |- (A.z z = y -> ([y / x]ph <-> [y / z][y / x]ph))
62		hbae 1505	. . . 4 |- (A.z z = y -> A.xA.z z = y)
63		sbequ12 1545	. . . . 5 |- (z = y -> (ph <-> [y / z]ph))
64	63	a4s 1330	. . . 4 |- (A.z z = y -> (ph <-> [y / z]ph))
65	62, 64	sbbid 1617	. . 3 |- (A.z z = y -> ([y / x]ph <-> [y / x][y / z]ph))
66	61, 65	bitr3d 589	. 2 |- (A.z z = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
67	52, 59, 66	pm2.61ii 144	1 |- ([y / z][y / x]ph <-> [y / x][y / z]ph)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296  [wsbc 1534

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-8 1306  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-11o 1588

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

Copyright terms: Public domain