MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exim Structured version   Unicode version

Theorem exim 1701
Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-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 id 23 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21aleximi 1700 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  eximi  1703  aleximiOLD  1706  19.23v  1810  19.8a  1910  19.8aOLD  1911  19.9ht  1942  19.23tOLD  1967  spimt  2061  elex2  3099  elex22  3100  vtoclegft  3159  spcimgft  3163  bj-axdd2  30967  bj-2exim  30990  bj-exlimh  30998  bj-alequex  31056  bj-spimtv  31066  wl-19.8a  31625  2exim  36380  pm11.71  36399  onfrALTlem2  36564  19.41rg  36569  ax6e2nd  36577  elex2VD  36889  elex22VD  36890  onfrALTlem2VD  36941  19.41rgVD  36954  ax6e2eqVD  36959  ax6e2ndVD  36960  ax6e2ndeqVD  36961  ax6e2ndALT  36982  ax6e2ndeqALT  36983
  Copyright terms: Public domain W3C validator