Theorem dvelimfALT2 1865

Description: Proof of dvelimf 2068 using dveeq2 1863 (shown as the last hypothesis) instead of ax12 1560. This shows that ax12 1560 could be replaced by dveeq2 1863 (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 1574	. . 3 |- ( -. A. x x = y -> A. z -. A. x x = y )
2		hbn1 1700	. . . 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 1621	. . 3 |- ( -. A. x x = y -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
7	1, 6	hbald 1539	. 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 1774	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
11	10	albii 1518	. 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 1395   = wceq 1397

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 619  ax-in2 620  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-fal 1403

This theorem is referenced by: (None)