Theorem dvelimfALT2 1839

Description: Proof of dvelimf 2042 using dveeq2 1837 (shown as the last hypothesis) instead of ax12 1534. This shows that ax12 1534 could be replaced by dveeq2 1837 (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 1548	. . 3 |- ( -. A. x x = y -> A. z -. A. x x = y )
2		hbn1 1674	. . . 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 1595	. . 3 |- ( -. A. x x = y -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
7	1, 6	hbald 1513	. 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 1748	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
11	10	albii 1492	. 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 1370   = wceq 1372

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-fal 1378

This theorem is referenced by: (None)