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

Theorem exim 1536
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 1479 . 2  |-  ( A. x ( ph  ->  ps )  ->  A. x A. x ( ph  ->  ps ) )
2 hbe1 1430 . 2  |-  ( E. x ps  ->  A. x E. x ps )
3 19.8a 1528 . . . 4  |-  ( ps 
->  E. x ps )
43imim2i 12 . . 3  |-  ( (
ph  ->  ps )  -> 
( ph  ->  E. x ps ) )
54sps 1476 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( ph  ->  E. x ps )
)
61, 2, 5exlimdh 1533 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1288   E.wex 1427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-ial 1473
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eximi  1537  exbi  1541  eximdh  1548  19.29  1557  19.25  1563  alexim  1582  19.23t  1613  spimt  1672  equvini  1689  nfexd  1692  ax10oe  1726  sbcof2  1739  spsbim  1772  mor  1991  rexim  2468  elex22  2635  elex2  2636  vtoclegft  2692  spcimgft  2696  spcimegft  2698  spc2gv  2710  spc3gv  2712  ssoprab2  5719  bj-inf2vnlem1  12138
  Copyright terms: Public domain W3C validator