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

Theorem exim 1573
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 1569 . . 3  |-  ( A. x  -.  ps  <->  -.  E. x ps )
4 alnex 1569 . . 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 1532   E.wex 1537
This theorem is referenced by:  eximi  1574  exbi  1579  eximdh  1586  19.29  1595  19.25  1602  19.30  1603  ax12o10lem14  1648  19.23t  1776  2mo  2196  elex22  2774  elex2  2775  vtoclegft  2830  cla4imgft  2834  ssoprab2  5838  2exim  26944  pm11.71  26963  onfrALTlem2  27364  19.41rg  27369  a9e2nd  27377  elex2VD  27664  elex22VD  27665  onfrALTlem2VD  27715  19.41rgVD  27728  a9e2eqVD  27733  a9e2ndVD  27734  a9e2ndeqVD  27735  a9e2ndALT  27757  a9e2ndeqALT  27758  ax12o10lem14K  28223  ax12o10lem14X  28224
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-ex 1538
  Copyright terms: Public domain W3C validator