Theorem dvelimfALT2 1804

Description: Proof of dvelimf 2002 using dveeq2 1802 (shown as the last hypothesis) instead of ax12 1499. This shows that ax12 1499 could be replaced by dveeq2 1802 (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 1513	. . 3 |- ( -. A. x x = y -> A. z -. A. x x = y )
2		hbn1 1639	. . . 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 1560	. . 3 |- ( -. A. x x = y -> ( ( z = y -> ph ) -> A. x ( z = y -> ph ) ) )
7	1, 6	hbald 1478	. 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 1713	. 2 |- ( A. z ( z = y -> ph ) <-> ps )
11	10	albii 1457	. 2 |- ( A. x A. z ( z = y -> ph ) <-> A. x ps )
12	7, 10, 11	3imtr3g 203	1 |- ( -. A. x x = y -> ( ps -> A. x ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   A.wal 1340   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-fal 1348

This theorem is referenced by: (None)