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

Theorem exim 1714
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 1712 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  eximi  1715  19.23v  1826  19.8a  1955  19.8aOLD  1956  19.9ht  1987  19.23tOLD  2012  spimt  2110  elex2  3044  elex22  3045  vtoclegft  3107  spcimgft  3111  bj-axdd2  31239  bj-2exim  31267  bj-exlimh  31275  bj-sbex  31303  bj-alequex  31375  bj-spimtv  31385  bj-spcimdv  31561  2exim  36798  pm11.71  36817  onfrALTlem2  36982  19.41rg  36987  ax6e2nd  36995  elex2VD  37297  elex22VD  37298  onfrALTlem2VD  37349  19.41rgVD  37362  ax6e2eqVD  37367  ax6e2ndVD  37368  ax6e2ndeqVD  37369  ax6e2ndALT  37390  ax6e2ndeqALT  37391
  Copyright terms: Public domain W3C validator