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

Theorem exim 1533
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 1476 . 2  |-  ( A. x ( ph  ->  ps )  ->  A. x A. x ( ph  ->  ps ) )
2 hbe1 1427 . 2  |-  ( E. x ps  ->  A. x E. x ps )
3 19.8a 1525 . . . 4  |-  ( ps 
->  E. x ps )
43imim2i 12 . . 3  |-  ( (
ph  ->  ps )  -> 
( ph  ->  E. x ps ) )
54sps 1473 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  E. x ps )
)
61, 2, 5exlimdh 1530 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285   E.wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eximi  1534  exbi  1538  eximdh  1545  19.29  1554  19.25  1560  alexim  1579  19.23t  1610  spimt  1668  equvini  1685  nfexd  1688  ax10oe  1722  sbcof2  1735  spsbim  1768  mor  1987  rexim  2463  elex22  2628  elex2  2629  vtoclegft  2684  spcimgft  2688  spcimegft  2690  spc2gv  2702  spc3gv  2704  ssoprab2  5662  bj-inf2vnlem1  11310
  Copyright terms: Public domain W3C validator