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

Theorem exim 1633
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 22 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21aleximi 1632 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  eximi  1635  aleximiOLD  1638  19.8a  1806  19.8aOLD  1807  19.9ht  1837  19.23t  1856  19.23v  1932  spimt  1974  2moOLDOLD  2384  elex2  3130  elex22  3131  vtoclegft  3190  spcimgft  3194  2exim  31186  pm11.71  31205  onfrALTlem2  32799  19.41rg  32804  ax6e2nd  32812  elex2VD  33119  elex22VD  33120  onfrALTlem2VD  33170  19.41rgVD  33183  ax6e2eqVD  33188  ax6e2ndVD  33189  ax6e2ndeqVD  33190  ax6e2ndALT  33211  ax6e2ndeqALT  33212  bj-axdd2  33663  bj-2exim  33691  bj-exlimh  33700  bj-alequex  33751  bj-spimtv  33761
  Copyright terms: Public domain W3C validator