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

Theorem exim 1565
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 1551 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( A. x  -.  ps  ->  A. x  -.  ph ) )
3 alnex 1533 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
4 alnex 1533 . . 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 1530   E.wex 1531
This theorem is referenced by:  eximi  1566  exbi  1571  eximdh  1578  19.29  1586  19.25  1593  19.30  1594  19.23h  1740  19.23t  1808  2mo  2234  elex22  2812  elex2  2813  vtoclegft  2868  spcimgft  2872  ssoprab2  5920  2exim  27680  pm11.71  27699  onfrALTlem2  28610  19.41rg  28615  a9e2nd  28623  elex2VD  28930  elex22VD  28931  onfrALTlem2VD  28981  19.41rgVD  28994  a9e2eqVD  28999  a9e2ndVD  29000  a9e2ndeqVD  29001  a9e2ndALT  29023  a9e2ndeqALT  29024
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator