ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvelimfALT2 Unicode version

Theorem dvelimfALT2 1840
Description: Proof of dvelimf 2043 using dveeq2 1838 (shown as the last hypothesis) instead of ax12 1535. This shows that ax12 1535 could be replaced by dveeq2 1838 (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
StepHypRef Expression
1 ax-17 1549 . . 3  |-  ( -. 
A. x  x  =  y  ->  A. z  -.  A. x  x  =  y )
2 hbn1 1675 . . . 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 )
54a1i 9 . . . 4  |-  ( -. 
A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
62, 3, 5hbimd 1596 . . 3  |-  ( -. 
A. x  x  =  y  ->  ( (
z  =  y  ->  ph )  ->  A. x
( z  =  y  ->  ph ) ) )
71, 6hbald 1514 . 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 ) )
108, 9equsalh 1749 . 2  |-  ( A. z ( z  =  y  ->  ph )  <->  ps )
1110albii 1493 . 2  |-  ( A. x A. z ( z  =  y  ->  ph )  <->  A. x ps )
127, 10, 113imtr3g 204 1  |-  ( -. 
A. x  x  =  y  ->  ( ps  ->  A. x ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 105   A.wal 1371    = wceq 1373
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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558
This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator