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

Theorem exim 1563
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 128 . . . 4  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
21al2imi 1549 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x  -.  ps  ->  A. x  -.  ph ) )
3 alnex 1531 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
4 alnex 1531 . . 3  |-  ( A. x  -.  ph  <->  -.  E. x ph )
52, 3, 43imtr3g 262 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( -.  E. x ps  ->  -.  E. x ph ) )
65con4d 99 1  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1528   E.wex 1529
This theorem is referenced by:  eximi  1564  exbi  1569  eximdh  1576  19.29  1584  19.25  1591  19.30  1592  19.23h  1729  19.23t  1797  2mo  2222  elex22  2800  elex2  2801  vtoclegft  2856  spcimgft  2860  ssoprab2  5865  2exim  26976  pm11.71  26995  onfrALTlem2  27582  19.41rg  27587  a9e2nd  27595  elex2VD  27882  elex22VD  27883  onfrALTlem2VD  27933  19.41rgVD  27946  a9e2eqVD  27951  a9e2ndVD  27952  a9e2ndeqVD  27953  a9e2ndALT  27975  a9e2ndeqALT  27976
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545
This theorem depends on definitions:  df-bi 179  df-ex 1530
  Copyright terms: Public domain W3C validator