Theorem sbcomxyyz 1843

Description: Version of sbcom 1846 with distinct variable constraints between x and y, and y and z. (Contributed by Jim Kingdon, 21-Mar-2018.)

Assertion

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

Distinct variable groups:   x,y   y,z

Allowed substitution hints:   ph(x,y,z)

Proof of Theorem sbcomxyyz

Step	Hyp	Ref	Expression
1		ax-bndl 1396	. 2 |- (A.z z = x \/ (A.z z = y \/ A.xA.z(x = y -> A.z x = y)))
2		ax-ial 1424	. . . . 5 |- (A.z z = x -> A.zA.z z = x)
3		drsb1 1677	. . . . 5 |- (A.z z = x -> ([y / z]ph <-> [y / x]ph))
4	2, 3	sbbid 1723	. . . 4 |- (A.z z = x -> ([y / z][y / z]ph <-> [y / z][y / x]ph))
5		drsb1 1677	. . . 4 |- (A.z z = x -> ([y / z][y / z]ph <-> [y / x][y / z]ph))
6	4, 5	bitr3d 179	. . 3 |- (A.z z = x -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
7		sbequ12 1651	. . . . . 6 |- (z = y -> ([y / x]ph <-> [y / z][y / x]ph))
8	7	sps 1427	. . . . 5 |- (A.z z = y -> ([y / x]ph <-> [y / z][y / x]ph))
9		hbae 1603	. . . . . 6 |- (A.z z = y -> A.xA.z z = y)
10		sbequ12 1651	. . . . . . 7 |- (z = y -> (ph <-> [y / z]ph))
11	10	sps 1427	. . . . . 6 |- (A.z z = y -> (ph <-> [y / z]ph))
12	9, 11	sbbid 1723	. . . . 5 |- (A.z z = y -> ([y / x]ph <-> [y / x][y / z]ph))
13	8, 12	bitr3d 179	. . . 4 |- (A.z z = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
14		df-nf 1347	. . . . . 6 |- ( F/z x = y <-> A.z(x = y -> A.z x = y))
15	14	albii 1356	. . . . 5 |- (A.x F/z x = y <-> A.xA.z(x = y -> A.z x = y))
16		ax-ial 1424	. . . . . . 7 |- (A.x F/z x = y -> A.xA.x F/z x = y)
17		nfs1v 1812	. . . . . . . . . 10 |- F/x[y / x]ph
18	17	nfsb 1819	. . . . . . . . 9 |- F/x[y / z][y / x]ph
19	18	a1i 9	. . . . . . . 8 |- (A.x F/z x = y -> F/x[y / z][y / x]ph)
20	19	nfrd 1410	. . . . . . 7 |- (A.x F/z x = y -> ([y / z][y / x]ph -> A.x[y / z][y / x]ph))
21		nfr 1408	. . . . . . . . 9 |- ( F/z x = y -> (x = y -> A.z x = y))
22		nfnf1 1433	. . . . . . . . . . . . 13 |- F/z F/z x = y
23		nfa1 1431	. . . . . . . . . . . . 13 |- F/zA.z x = y
24	22, 23	nfan 1454	. . . . . . . . . . . 12 |- F/z( F/z x = y /\ A.z x = y)
25	24	nfri 1409	. . . . . . . . . . 11 |- (( F/z x = y /\ A.z x = y) -> A.z( F/z x = y /\ A.z x = y))
26		nfs1v 1812	. . . . . . . . . . . . 13 |- F/z[y / z][y / x]ph
27	26	a1i 9	. . . . . . . . . . . 12 |- (( F/z x = y /\ A.z x = y) -> F/z[y / z][y / x]ph)
28	27	nfrd 1410	. . . . . . . . . . 11 |- (( F/z x = y /\ A.z x = y) -> ([y / z][y / x]ph -> A.z[y / z][y / x]ph))
29		sbequ12 1651	. . . . . . . . . . . . . . 15 |- (x = y -> (ph <-> [y / x]ph))
30	29, 7	sylan9bb 435	. . . . . . . . . . . . . 14 |- ((x = y /\ z = y) -> (ph <-> [y / z][y / x]ph))
31	30	ex 108	. . . . . . . . . . . . 13 |- (x = y -> (z = y -> (ph <-> [y / z][y / x]ph)))
32	31	sps 1427	. . . . . . . . . . . 12 |- (A.z x = y -> (z = y -> (ph <-> [y / z][y / x]ph)))
33	32	adantl 262	. . . . . . . . . . 11 |- (( F/z x = y /\ A.z x = y) -> (z = y -> (ph <-> [y / z][y / x]ph)))
34	25, 28, 33	sbiedh 1667	. . . . . . . . . 10 |- (( F/z x = y /\ A.z x = y) -> ([y / z]ph <-> [y / z][y / x]ph))
35	34	ex 108	. . . . . . . . 9 |- ( F/z x = y -> (A.z x = y -> ([y / z]ph <-> [y / z][y / x]ph)))
36	21, 35	syld 40	. . . . . . . 8 |- ( F/z x = y -> (x = y -> ([y / z]ph <-> [y / z][y / x]ph)))
37	36	sps 1427	. . . . . . 7 |- (A.x F/z x = y -> (x = y -> ([y / z]ph <-> [y / z][y / x]ph)))
38	16, 20, 37	sbiedh 1667	. . . . . 6 |- (A.x F/z x = y -> ([y / x][y / z]ph <-> [y / z][y / x]ph))
39	38	bicomd 129	. . . . 5 |- (A.x F/z x = y -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
40	15, 39	sylbir 125	. . . 4 |- (A.xA.z(x = y -> A.z x = y) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
41	13, 40	jaoi 635	. . 3 |- ((A.z z = y \/ A.xA.z(x = y -> A.z x = y)) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
42	6, 41	jaoi 635	. 2 |- ((A.z z = x \/ (A.z z = y \/ A.xA.z(x = y -> A.z x = y))) -> ([y / z][y / x]ph <-> [y / x][y / z]ph))
43	1, 42	ax-mp 7	1 |- ([y / z][y / x]ph <-> [y / x][y / z]ph)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628  A.wal 1240   F/wnf 1346  [wsb 1642

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  sbco3xzyz  1844