Theorem rexim 3008

Description: Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rexim	|- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )

Proof of Theorem rexim

Step	Hyp	Ref	Expression
1		con3 149	. . . 4 |- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2	1	ral2imi 2947	. . 3 |- ( A. x e. A ( ph -> ps ) -> ( A. x e. A -. ps -> A. x e. A -. ph ) )
3	2	con3d 148	. 2 |- ( A. x e. A ( ph -> ps ) -> ( -. A. x e. A -. ph -> -. A. x e. A -. ps ) )
4		dfrex2 2996	. 2 |- ( E. x e. A ph <-> -. A. x e. A -. ph )
5		dfrex2 2996	. 2 |- ( E. x e. A ps <-> -. A. x e. A -. ps )
6	3, 4, 5	3imtr4g 285	1 |- ( A. x e. A ( ph -> ps ) -> ( E. x e. A ph -> E. x e. A ps ) )

Syntax hints:   -. wn 3   -> wi 4   A.wral 2912   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  reximia  3009  reximdai  3012  reximdvai  3015  r19.29  3072  reupick2  3913  ss2iun  4536  chfnrn  6328  isf32lem2  9176  ptcmplem4  21859  bnj110  30928  poimirlem25  33434