Theorem dvelimv 1939

Description: Similar to dvelim 2016 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.)

Hypothesis

Ref	Expression
dvelimv.1	|- (z = y -> (ph <-> ps))

Assertion

Ref	Expression
dvelimv	|- (-. A.x x = y -> (ps -> A.xps))

Distinct variable groups:   x,z   y,z   ps,z   ph,x

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

Proof of Theorem dvelimv

Step	Hyp	Ref	Expression
1		ax-17 1616	. . . . . 6 |- (ps -> A.zps)
2	1	a1d 22	. . . . . 6 |- (ps -> (z = y -> A.zps))
3	1, 2	alrimih 1565	. . . . 5 |- (ps -> A.z(z = y -> A.zps))
4		sp 1747	. . . . . . . 8 |- (A.zps -> ps)
5		dvelimv.1	. . . . . . . 8 |- (z = y -> (ph <-> ps))
6	4, 5	syl5ibr 212	. . . . . . 7 |- (z = y -> (A.zps -> ph))
7	6	a2i 12	. . . . . 6 |- ((z = y -> A.zps) -> (z = y -> ph))
8	7	alimi 1559	. . . . 5 |- (A.z(z = y -> A.zps) -> A.z(z = y -> ph))
9	3, 8	syl 15	. . . 4 |- (ps -> A.z(z = y -> ph))
10		ax10lem3 1938	. . . . . . . 8 |- (A.z z = x -> A.x x = z)
11	10	con3i 127	. . . . . . 7 |- (-. A.x x = z -> -. A.z z = x)
12		hbn1 1730	. . . . . . . 8 |- (-. A.z z = x -> A.z -. A.z z = x)
13		ax10lem3 1938	. . . . . . . . 9 |- (A.x x = z -> A.z z = x)
14	13	con3i 127	. . . . . . . 8 |- (-. A.z z = x -> -. A.x x = z)
15	12, 14	alrimih 1565	. . . . . . 7 |- (-. A.z z = x -> A.z -. A.x x = z)
16	11, 15	syl 15	. . . . . 6 |- (-. A.x x = z -> A.z -. A.x x = z)
17		ax-17 1616	. . . . . 6 |- (-. A.x x = y -> A.z -. A.x x = y)
18	16, 17	hban 1828	. . . . 5 |- ((-. A.x x = z /\ -. A.x x = y) -> A.z(-. A.x x = z /\ -. A.x x = y))
19		hbn1 1730	. . . . . . 7 |- (-. A.x x = z -> A.x -. A.x x = z)
20		hbn1 1730	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
21	19, 20	hban 1828	. . . . . 6 |- ((-. A.x x = z /\ -. A.x x = y) -> A.x(-. A.x x = z /\ -. A.x x = y))
22		ax12o 1934	. . . . . . 7 |- (-. A.x x = z -> (-. A.x x = y -> (z = y -> A.x z = y)))
23	22	imp 418	. . . . . 6 |- ((-. A.x x = z /\ -. A.x x = y) -> (z = y -> A.x z = y))
24		a17d 1617	. . . . . 6 |- ((-. A.x x = z /\ -. A.x x = y) -> (ph -> A.xph))
25	21, 23, 24	hbimd 1815	. . . . 5 |- ((-. A.x x = z /\ -. A.x x = y) -> ((z = y -> ph) -> A.x(z = y -> ph)))
26	18, 25	hbald 1740	. . . 4 |- ((-. A.x x = z /\ -. A.x x = y) -> (A.z(z = y -> ph) -> A.xA.z(z = y -> ph)))
27	5	biimpd 198	. . . . . . . . 9 |- (z = y -> (ph -> ps))
28	27	a2i 12	. . . . . . . 8 |- ((z = y -> ph) -> (z = y -> ps))
29	28	alimi 1559	. . . . . . 7 |- (A.z(z = y -> ph) -> A.z(z = y -> ps))
30		ax9v 1655	. . . . . . . 8 |- -. A.z -. z = y
31		con3 126	. . . . . . . . 9 |- ((z = y -> ps) -> (-. ps -> -. z = y))
32	31	al2imi 1561	. . . . . . . 8 |- (A.z(z = y -> ps) -> (A.z -. ps -> A.z -. z = y))
33	30, 32	mtoi 169	. . . . . . 7 |- (A.z(z = y -> ps) -> -. A.z -. ps)
34	29, 33	syl 15	. . . . . 6 |- (A.z(z = y -> ph) -> -. A.z -. ps)
35		ax-17 1616	. . . . . 6 |- (-. ps -> A.z -. ps)
36	34, 35	nsyl2 119	. . . . 5 |- (A.z(z = y -> ph) -> ps)
37	36	alimi 1559	. . . 4 |- (A.xA.z(z = y -> ph) -> A.xps)
38	9, 26, 37	syl56 30	. . 3 |- ((-. A.x x = z /\ -. A.x x = y) -> (ps -> A.xps))
39	38	expcom 424	. 2 |- (-. A.x x = y -> (-. A.x x = z -> (ps -> A.xps)))
40		sp 1747	. . . 4 |- (A.x x = z -> x = z)
41		ax-11 1746	. . . 4 |- (x = z -> (A.zps -> A.x(x = z -> ps)))
42	40, 1, 41	syl2im 34	. . 3 |- (A.x x = z -> (ps -> A.x(x = z -> ps)))
43		pm2.27 35	. . . 4 |- (x = z -> ((x = z -> ps) -> ps))
44	43	al2imi 1561	. . 3 |- (A.x x = z -> (A.x(x = z -> ps) -> A.xps))
45	42, 44	syld 40	. 2 |- (A.x x = z -> (ps -> A.xps))
46	39, 45	pm2.61d2 152	1 |- (-. A.x x = y -> (ps -> A.xps))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540

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

This theorem is referenced by:  dveeq2  1940  ax10lem4  1941  dveeq1  2018  dveel1  2019  dveel2  2020  rgen2a  2680