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

Theorem exim 1706
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 1704 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1442   E.wex 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  eximi  1707  19.23v  1818  19.8a  1935  19.8aOLD  1936  19.9ht  1967  19.23tOLD  1992  spimt  2097  elex2  3058  elex22  3059  vtoclegft  3121  spcimgft  3125  bj-axdd2  31175  bj-2exim  31203  bj-exlimh  31211  bj-sbex  31239  bj-alequex  31309  bj-spimtv  31319  bj-spcimdv  31493  wl-19.8a  31910  2exim  36728  pm11.71  36747  onfrALTlem2  36912  19.41rg  36917  ax6e2nd  36925  elex2VD  37234  elex22VD  37235  onfrALTlem2VD  37286  19.41rgVD  37299  ax6e2eqVD  37304  ax6e2ndVD  37305  ax6e2ndeqVD  37306  ax6e2ndALT  37327  ax6e2ndeqALT  37328
  Copyright terms: Public domain W3C validator