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

Theorem exim 1562
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 con3 126 . . . 4  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
21al2imi 1548 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x  -.  ps  ->  A. x  -.  ph ) )
3 alnex 1530 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
4 alnex 1530 . . 3  |-  ( A. x  -.  ph  <->  -.  E. x ph )
52, 3, 43imtr3g 260 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( -.  E. x ps  ->  -.  E. x ph ) )
65con4d 97 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527   E.wex 1528
This theorem is referenced by:  eximi  1563  exbi  1568  eximdh  1575  19.29  1583  19.25  1590  19.30  1591  19.23h  1728  19.23t  1796  2mo  2221  elex22  2799  elex2  2800  vtoclegft  2855  spcimgft  2859  ssoprab2  5904  2exim  27577  pm11.71  27596  onfrALTlem2  28311  19.41rg  28316  a9e2nd  28324  elex2VD  28614  elex22VD  28615  onfrALTlem2VD  28665  19.41rgVD  28678  a9e2eqVD  28683  a9e2ndVD  28684  a9e2ndeqVD  28685  a9e2ndALT  28707  a9e2ndeqALT  28708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator