Theorem sbcom 2089

Description: A commutativity law for substitution. (Contributed by NM, 27-May-1997.)

Assertion

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

Proof of Theorem sbcom

Step	Hyp	Ref	Expression
1		drsb1 2022	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / z][y / x]ph))
2		nfae 1954	. . . . . . 7 |- F/xA.x x = z
3		drsb1 2022	. . . . . . 7 |- (A.x x = z -> ([y / x]ph <-> [y / z]ph))
4	2, 3	sbbid 2078	. . . . . 6 |- (A.x x = z -> ([y / x][y / x]ph <-> [y / x][y / z]ph))
5	1, 4	bitr3d 246	. . . . 5 |- (A.x x = z -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
6	5	adantr 451	. . . 4 |- ((A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
7		nfnae 1956	. . . . . . . . 9 |- F/z -. A.x x = z
8		nfnae 1956	. . . . . . . . 9 |- F/z -. A.x x = y
9	7, 8	nfan 1824	. . . . . . . 8 |- F/z(-. A.x x = z /\ -. A.x x = y)
10		nfeqf 1958	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.x x = y) -> F/x z = y)
11		19.21t 1795	. . . . . . . . 9 |- ( F/x z = y -> (A.x(z = y -> (x = y -> ph)) <-> (z = y -> A.x(x = y -> ph))))
12	10, 11	syl 15	. . . . . . . 8 |- ((-. A.x x = z /\ -. A.x x = y) -> (A.x(z = y -> (x = y -> ph)) <-> (z = y -> A.x(x = y -> ph))))
13	9, 12	albid 1772	. . . . . . 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))))
14	13	adantrr 697	. . . . . 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))))
15		alcom 1737	. . . . . . . 8 |- (A.zA.x(z = y -> (x = y -> ph)) <-> A.xA.z(z = y -> (x = y -> ph)))
16		nfnae 1956	. . . . . . . . . 10 |- F/x -. A.x x = z
17		nfnae 1956	. . . . . . . . . 10 |- F/x -. A.z z = y
18	16, 17	nfan 1824	. . . . . . . . 9 |- F/x(-. A.x x = z /\ -. A.z z = y)
19		bi2.04 350	. . . . . . . . . . 11 |- ((z = y -> (x = y -> ph)) <-> (x = y -> (z = y -> ph)))
20	19	albii 1566	. . . . . . . . . 10 |- (A.z(z = y -> (x = y -> ph)) <-> A.z(x = y -> (z = y -> ph)))
21		aecom 1946	. . . . . . . . . . . . 13 |- (A.z z = x -> A.x x = z)
22	21	con3i 127	. . . . . . . . . . . 12 |- (-. A.x x = z -> -. A.z z = x)
23		nfeqf 1958	. . . . . . . . . . . 12 |- ((-. A.z z = x /\ -. A.z z = y) -> F/z x = y)
24	22, 23	sylan 457	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.z z = y) -> F/z x = y)
25		19.21t 1795	. . . . . . . . . . 11 |- ( F/z x = y -> (A.z(x = y -> (z = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
26	24, 25	syl 15	. . . . . . . . . 10 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.z(x = y -> (z = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
27	20, 26	syl5bb 248	. . . . . . . . 9 |- ((-. A.x x = z /\ -. A.z z = y) -> (A.z(z = y -> (x = y -> ph)) <-> (x = y -> A.z(z = y -> ph))))
28	18, 27	albid 1772	. . . . . . . 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))))
29	15, 28	syl5bb 248	. . . . . . 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))))
30	29	adantrl 696	. . . . . 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))))
31	14, 30	bitr3d 246	. . . . 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))))
32		sb4b 2054	. . . . . . 7 |- (-. A.z z = y -> ([y / z][y / x]ph <-> A.z(z = y -> [y / x]ph)))
33		sb4b 2054	. . . . . . . . 9 |- (-. A.x x = y -> ([y / x]ph <-> A.x(x = y -> ph)))
34	33	imbi2d 307	. . . . . . . 8 |- (-. A.x x = y -> ((z = y -> [y / x]ph) <-> (z = y -> A.x(x = y -> ph))))
35	8, 34	albid 1772	. . . . . . 7 |- (-. A.x x = y -> (A.z(z = y -> [y / x]ph) <-> A.z(z = y -> A.x(x = y -> ph))))
36	32, 35	sylan9bbr 681	. . . . . 6 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> A.z(z = y -> A.x(x = y -> ph))))
37	36	adantl 452	. . . . 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))))
38		sb4b 2054	. . . . . . 7 |- (-. A.x x = y -> ([y / x][y / z]ph <-> A.x(x = y -> [y / z]ph)))
39		sb4b 2054	. . . . . . . . 9 |- (-. A.z z = y -> ([y / z]ph <-> A.z(z = y -> ph)))
40	39	imbi2d 307	. . . . . . . 8 |- (-. A.z z = y -> ((x = y -> [y / z]ph) <-> (x = y -> A.z(z = y -> ph))))
41	17, 40	albid 1772	. . . . . . 7 |- (-. A.z z = y -> (A.x(x = y -> [y / z]ph) <-> A.x(x = y -> A.z(z = y -> ph))))
42	38, 41	sylan9bb 680	. . . . . 6 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / x][y / z]ph <-> A.x(x = y -> A.z(z = y -> ph))))
43	42	adantl 452	. . . . 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))))
44	31, 37, 43	3bitr4d 276	. . . 4 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.z z = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
45	6, 44	pm2.61ian 765	. . 3 |- ((-. A.x x = y /\ -. A.z z = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
46	45	ex 423	. 2 |- (-. A.x x = y -> (-. A.z z = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph)))
47		nfae 1954	. . . 4 |- F/zA.x x = y
48		sbequ12 1919	. . . . 5 |- (x = y -> (ph <-> [y / x]ph))
49	48	sps 1754	. . . 4 |- (A.x x = y -> (ph <-> [y / x]ph))
50	47, 49	sbbid 2078	. . 3 |- (A.x x = y -> ([y / z]ph <-> [y / z][y / x]ph))
51		sbequ12 1919	. . . 4 |- (x = y -> ([y / z]ph <-> [y / x][y / z]ph))
52	51	sps 1754	. . 3 |- (A.x x = y -> ([y / z]ph <-> [y / x][y / z]ph))
53	50, 52	bitr3d 246	. 2 |- (A.x x = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
54		sbequ12 1919	. . . 4 |- (z = y -> ([y / x]ph <-> [y / z][y / x]ph))
55	54	sps 1754	. . 3 |- (A.z z = y -> ([y / x]ph <-> [y / z][y / x]ph))
56		nfae 1954	. . . 4 |- F/xA.z z = y
57		sbequ12 1919	. . . . 5 |- (z = y -> (ph <-> [y / z]ph))
58	57	sps 1754	. . . 4 |- (A.z z = y -> (ph <-> [y / z]ph))
59	56, 58	sbbid 2078	. . 3 |- (A.z z = y -> ([y / x]ph <-> [y / x][y / z]ph))
60	55, 59	bitr3d 246	. 2 |- (A.z z = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
61	46, 53, 60	pm2.61ii 157	1 |- ([y / z][y / x]ph <-> [y / x][y / z]ph)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540   F/wnf 1544  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by: (None)