Theorem dvelimfALT2 1831

Description: Proof of dvelimf 2034 using dveeq2 1829 (shown as the last hypothesis) instead of ax12 1526. This shows that ax12 1526 could be replaced by dveeq2 1829 (the last hypothesis). (Contributed by Andrew Salmon, 21-Jul-2011.)

Hypotheses

Ref	Expression
dvelimfALT2.1	|- ( ph -> A. x ph )
dvelimfALT2.2	|- ( ps -> A. z ps )
dvelimfALT2.3	|- ( z = y -> ( ph <-> ps ) )
dvelimfALT2.4	|- ( -. A. x x = y -> ( z = y -> A. x z = y ) )

Assertion

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

Distinct variable groups:   x, z   y, z

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

Proof of Theorem dvelimfALT2

Step	Hyp	Ref	Expression
1		ax-17 1540	. . 3 |- ( -. A. x x = y -> A. z -. A. x x = y )
2		hbn1 1666	. . . 4 |- ( -. A. x x = y -> A. x -. A. x x = y )
3		dvelimfALT2.4	. . . 4 |- ( -. A. x x = y -> ( z = y -> A. x z = y ) )
4		dvelimfALT2.1	. . . . 5 |- ( ph -> A. x ph )
5	4	a1i 9	. . . 4 |- ( -. A. x x = y -> ( ph -> A. x ph ) )
6	2, 3, 5	hbimd 1587	. . 3 |- ( -. A. x x = y -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
7	1, 6	hbald 1505	. 2 |- ( -. A. x x = y -> ( A. z ( z = y -> ph ) -> A. x A. z ( z = y -> ph ) ) )
8		dvelimfALT2.2	. . 3 |- ( ps -> A. z ps )
9		dvelimfALT2.3	. . 3 |- ( z = y -> ( ph <-> ps ) )
10	8, 9	equsalh 1740	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
11	10	albii 1484	. 2 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
12	7, 10, 11	3imtr3g 204	1 |- ( -. A. x x = y -> ( ps -> A. x ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   A.wal 1362   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-fal 1370

This theorem is referenced by: (None)