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

Theorem exim 1563
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
exim  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )

Proof of Theorem exim
StepHypRef Expression
1 hba1 1505 . 2  |-  ( A. x ( ph  ->  ps )  ->  A. x A. x ( ph  ->  ps ) )
2 hbe1 1456 . 2  |-  ( E. x ps  ->  A. x E. x ps )
3 19.8a 1554 . . . 4  |-  ( ps 
->  E. x ps )
43imim2i 12 . . 3  |-  ( (
ph  ->  ps )  -> 
( ph  ->  E. x ps ) )
54sps 1502 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  E. x ps )
)
61, 2, 5exlimdh 1560 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1314   E.wex 1453
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-ial 1499
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eximi  1564  exbi  1568  eximdh  1575  19.29  1584  19.25  1590  alexim  1609  19.23t  1640  spimt  1699  equvini  1716  nfexd  1719  ax10oe  1753  sbcof2  1766  spsbim  1799  mor  2019  rexim  2503  elex22  2675  elex2  2676  vtoclegft  2732  spcimgft  2736  spcimegft  2738  spc2gv  2750  spc3gv  2752  ssoprab2  5795  bj-inf2vnlem1  13095
  Copyright terms: Public domain W3C validator