Theorem sbcom 916

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		del43b 857	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / z][y / x]ph))
2		eq5 824	. . . . . . 7 |- (A.x x = z -> A.xA.x x = z)
3		del43b 857	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
4	2, 3	bisbd 897	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / x][y / z]ph))
5	1, 4	bitr3d 408	. . . . 5 |- (A.x x = z -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
6	5	a1d 14	. . . 4 |- (A.x x = z -> ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph)))
7		eq6 826	. . . . . . . . . 10 |- (-. A.x x = z -> A.z -. A.x x = z)
8		eq6 826	. . . . . . . . . 10 |- (-. A.x x = y -> A.z -. A.x x = y)
9	7, 8	hban 704	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.x x = y) -> A.z(-. A.x x = z /\ -. A.x x = y))
10		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = z -> A.x -. A.x x = z)
11		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = y -> A.x -. A.x x = y)
12	10, 11	hban 704	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.x x = y) -> A.x(-. A.x x = z /\ -. A.x x = y))
13		ax-12 802	. . . . . . . . . . . 12 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
14	13	imp 277	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.x x = y) -> (z = y -> A.x z = y))
15	14	19.20i 691	. . . . . . . . . 10 |- (A.x(-. A.x x = z /\ -. A.x x = y) -> A.x(z = y -> A.x z = y))
16		19.21g 792	. . . . . . . . . 10 |- (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 21	. . . . . . . . 9 |- ((-. 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	biald 782	. . . . . . . 8 |- ((-. 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 312	. . . . . . 7 |- ((-. 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		eq6 826	. . . . . . . . . . 11 |- (-. A.z z = y -> A.x -. A.z z = y)
21	10, 20	hban 704	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.z z = y) -> A.x(-. A.x x = z /\ -. A.z z = y))
22		eq6 826	. . . . . . . . . . . . 13 |- (-. A.z z = y -> A.z -. A.z z = y)
23	7, 22	hban 704	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ -. A.z z = y) -> A.z(-. A.x x = z /\ -. A.z z = y))
24		ax-12 802	. . . . . . . . . . . . . . 15 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
25	24	eq4ds 823	. . . . . . . . . . . . . 14 |- (-. A.x x = z -> (-. A.z z = y -> (x = y -> A.z x = y)))
26	25	imp 277	. . . . . . . . . . . . 13 |- ((-. A.x x = z /\ -. A.z z = y) -> (x = y -> A.z x = y))
27	26	19.20i 691	. . . . . . . . . . . 12 |- (A.z(-. A.x x = z /\ -. A.z z = y) -> A.z(x = y -> A.z x = y))
28		19.21g 792	. . . . . . . . . . . 12 |- (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 21	. . . . . . . . . . 11 |- ((-. 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 141	. . . . . . . . . . . 12 |- ((z = y -> (x = y -> ph)) <-> (x = y -> (z = y -> ph)))
31	30	bial 695	. . . . . . . . . . 11 |- (A.z(z = y -> (x = y -> ph)) <-> A.z(x = y -> (z = y -> ph)))
32	29, 31	syl5bb 410	. . . . . . . . . 10 |- ((-. 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	biald 782	. . . . . . . . 9 |- ((-. 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 715	. . . . . . . . 9 |- (A.zA.x(z = y -> (x = y -> ph)) <-> A.xA.z(z = y -> (x = y -> ph)))
35	33, 34	syl5bb 410	. . . . . . . 8 |- ((-. 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 311	. . . . . . 7 |- ((-. 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 408	. . . . . 6 |- ((-. 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 862	. . . . . . . 8 |- (-. A.z z = y -> ([y / z][y / x]ph <-> A.z(z = y -> [y / x]ph)))
39		sb4b 862	. . . . . . . . . 10 |- (-. A.x x = y -> ([y / x]ph <-> A.x(x = y -> ph)))
40	39	imbi2d 464	. . . . . . . . 9 |- (-. A.x x = y -> ((z = y -> [y / x]ph) <-> (z = y -> A.x(x = y -> ph))))
41	8, 40	biald 782	. . . . . . . 8 |- (-. A.x x = y -> (A.z(z = y -> [y / x]ph) <-> A.z(z = y -> A.x(x = y -> ph))))
42	38, 41	sylan9bbr 419	. . . . . . 7 |- ((-. 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 305	. . . . . 6 |- ((-. 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 862	. . . . . . . 8 |- (-. A.x x = y -> ([y / x][y / z]ph <-> A.x(x = y -> [y / z]ph)))
45		sb4b 862	. . . . . . . . . 10 |- (-. A.z z = y -> ([y / z]ph <-> A.z(z = y -> ph)))
46	45	imbi2d 464	. . . . . . . . 9 |- (-. A.z z = y -> ((x = y -> [y / z]ph) <-> (x = y -> A.z(z = y -> ph))))
47	20, 46	biald 782	. . . . . . . 8 |- (-. A.z z = y -> (A.x(x = y -> [y / z]ph) <-> A.x(x = y -> A.z(z = y -> ph))))
48	44, 47	sylan9bb 418	. . . . . . 7 |- ((-. 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 305	. . . . . 6 |- ((-. 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 424	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
51	50	exp 291	. . . 4 |- (-. A.x x = z -> ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph)))
52	6, 51	pm2.61i 110	. . 3 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
53	52	exp 291	. 2 |- (-. A.x x =