Theorem sbcom 1253

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 1171	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / z][y / x]ph))
2		hbae 1141	. . . . . . 7 |- (A.x x = z -> A.xA.x x = z)
3		drsb1 1171	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
4	2, 3	sbbid 1241	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / x][y / z]ph))
5	1, 4	bitr3d 528	. . . . 5 |- (A.x x = z -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
6	5	adantr 389	. . . 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 1143	. . . . . . . . 9 |- (-. A.x x = z -> A.z -. A.x x = z)
8		hbnae 1143	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
9	7, 8	hban 1006	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> A.z(-. A.x x = z /\ -. A.x x = y))
10		hbnae 1143	. . . . . . . . . 10 |- (-. A.x x = z -> A.x -. A.x x = z)
11		hbnae 1143	. . . . . . . . . 10 |- (-. A.x x = y -> A.x -. A.x x = y)
12	10, 11	hban 1006	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.x x = y) -> A.x(-. A.x x = z /\ -. A.x x = y))
13		ax-12 965	. . . . . . . . . . 11 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
14	13	imp 350	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.x x = y) -> (z = y -> A.x z = y))
15	14	19.20i 989	. . . . . . . . 9 |- (A.x(-. A.x x = z /\ -. A.x x = y) -> A.x(z = y -> A.x z = y))
16		19.21t 1111	. . . . . . . . 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 20	. . . . . . . 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 1100	. . . . . . 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 395	. . . . . 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 1143	. . . . . . . . . 10 |- (-. A.z z = y -> A.x -. A.z z = y)
21	10, 20	hban 1006	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.z z = y) -> A.x(-. A.x x = z /\ -. A.z z = y))
22		hbnae 1143	. . . . . . . . . . . 12 |- (-. A.z z = y -> A.z -. A.z z = y)
23	7, 22	hban 1006	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.z z = y) -> A.z(-. A.x x = z /\ -. A.z z = y))
24		ax-12 965	. . . . . . . . . . . . . 14 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
25	24	nalequcoms 1140	. . . . . . . . . . . . 13 |- (-. A.x x = z -> (-. A.z z = y -> (x = y -> A.z x = y)))
26	25	imp 350	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ -. A.z z = y) -> (x = y -> A.z x = y))
27	26	19.20i 989	. . . . . . . . . . 11 |- (A.z(-. A.x x = z /\ -. A.z z = y) -> A.z(x = y -> A.z x = y))
28		19.21t 1111	. . . . . . . . . . 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 20	. . . . . . . . . 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 160	. . . . . . . . . . 11 |- ((z = y -> (x = y -> ph)) <-> (x = y -> (z = y -> ph)))
31	30	albii 996	. . . . . . . . . 10 |- (A.z(z = y -> (x = y -> ph)) <-> A.z(x = y -> (z = y -> ph)))
32	29, 31	syl5bb 530	. . . . . . . . 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 1100	. . . . . . . 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 1028	. . . . . . . 8 |- (A.zA.x(z = y -> (x = y -> ph)) <-> A.xA.z(z = y -> (x = y -> ph)))
35	33, 34	syl5bb 530	. . . . . . 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 394	. . . . . 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 528	. . . . 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 1219	. . . . . . 7 |- (-. A.z z = y -> ([y / z][y / x]ph <-> A.z(z = y -> [y / x]ph)))
39		sb4b 1219	. . . . . . . . 9 |- (-. A.x x = y -> ([y / x]ph <-> A.x(x = y -> ph)))
40	39	imbi2d 610	. . . . . . . 8 |- (-. A.x x = y -> ((z = y -> [y / x]ph) <-> (z = y -> A.x(x = y -> ph))))
41	8, 40	albid 1100	. . . . . . 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 539	. . . . . 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 388	. . . . 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 1219	. . . . . . 7 |- (-. A.x x = y -> ([y / x][y / z]ph <-> A.x(x = y -> [y / z]ph)))
45		sb4b 1219	. . . . . . . . 9 |- (-. A.z z = y -> ([y / z]ph <-> A.z(z = y -> ph)))
46	45	imbi2d 610	. . . . . . . 8 |- (-. A.z z = y -> ((x = y -> [y / z]ph) <-> (x = y -> A.z(z = y -> ph))))
47	20, 46	albid 1100	. . . . . . 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 538	. . . . . 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 388	. . . . 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 548	. . . 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 475	. . 3 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
52	51