Theorem ddelimdf 909

Description: Deduction form of ddelimf 908. This version may be useful if we want to avoid ax-17 925 and use ax-16 922 instead.

Hypotheses

Ref	Expression
ddelimdf.1	|- (ph -> A.xph)
ddelimdf.2	|- (ph -> A.zph)
ddelimdf.3	|- (ph -> (ps -> A.xps))
ddelimdf.4	|- (ph -> (ch -> A.zch))
ddelimdf.5	|- (ph -> (z = y -> (ps <-> ch)))

Assertion

Ref	Expression
ddelimdf	|- (ph -> (-. A.x x = y -> (ch -> A.xch)))

Proof of Theorem ddelimdf

Step	Hyp	Ref	Expression
1		ddelimdf.2	. . . . . 6 |- (ph -> A.zph)
2		ddelimdf.1	. . . . . 6 |- (ph -> A.xph)
3	1, 2	19.21ai 740	. . . . 5 |- (ph -> A.zA.xph)
4		ddelimdf.3	. . . . . . 7 |- (ph -> (ps -> A.xps))
5	4	19.20i 691	. . . . . 6 |- (A.xph -> A.x(ps -> A.xps))
6	5	19.20i 691	. . . . 5 |- (A.zA.xph -> A.zA.x(ps -> A.xps))
7		hbsb4t 906	. . . . 5 |- (A.zA.x(ps -> A.xps) -> (-. A.x x = y -> ([y / z]ps -> A.x[y / z]ps)))
8	3, 6, 7	3syl 21	. . . 4 |- (ph -> (-. A.x x = y -> ([y / z]ps -> A.x[y / z]ps)))
9	8	imp 277	. . 3 |- ((ph /\ -. A.x x = y) -> ([y / z]ps -> A.x[y / z]ps))
10		ddelimdf.4	. . . . 5 |- (ph -> (ch -> A.zch))
11		ddelimdf.5	. . . . 5 |- (ph -> (z = y -> (ps <-> ch)))
12	1, 10, 11	sbied 903	. . . 4 |- (ph -> ([y / z]ps <-> ch))
13	12	adantr 306	. . 3 |- ((ph /\ -. A.x x = y) -> ([y / z]ps <-> ch))
14	2, 12	biald 782	. . . 4 |- (ph -> (A.x[y / z]ps <-> A.xch))
15	14	adantr 306	. . 3 |- ((ph /\ -. A.x x = y) -> (A.x[y / z]ps <-> A.xch))
16	9, 13, 15	3imtr3d 420	. 2 |- ((ph /\ -. A.x x = y) -> (ch -> A.xch))
17	16	exp 291	1 |- (ph -> (-. A.x x = y -> (ch -> A.xch)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672   = weq 797  [wsb 852

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org