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

Theorem exim 1585
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 129 . . . 4  |-  ( (
ph  ->  ps )  -> 
( -.  ps  ->  -. 
ph ) )
21al2imi 1571 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x  -.  ps  ->  A. x  -.  ph ) )
3 alnex 1553 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
4 alnex 1553 . . 3  |-  ( A. x  -.  ph  <->  -.  E. x ph )
52, 3, 43imtr3g 262 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( -.  E. x ps  ->  -.  E. x ph ) )
65con4d 100 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 1550   E.wex 1551
This theorem is referenced by:  eximi  1586  exbi  1592  eximdh  1599  19.29  1607  19.25  1614  19.30  1615  19.8a  1763  19.9ht  1793  19.23t  1819  19.23tOLD  1839  19.23hOLD  1840  spimt  1956  2mo  2361  elex22  2969  elex2  2970  vtoclegft  3025  spcimgft  3029  ssoprab2  6132  2exim  27556  pm11.71  27575  onfrALTlem2  28634  19.41rg  28639  a9e2nd  28647  elex2VD  28952  elex22VD  28953  onfrALTlem2VD  29003  19.41rgVD  29016  a9e2eqVD  29021  a9e2ndVD  29022  a9e2ndeqVD  29023  a9e2ndALT  29044  a9e2ndeqALT  29045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator