Theorem reximdai 2933

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)

Hypotheses

Ref	Expression
reximdai.1	|- F/ x ph
reximdai.2	|- ( ph -> ( x e. A -> ( ps -> ch ) ) )

Assertion

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

Proof of Theorem reximdai

Step	Hyp	Ref	Expression
1		reximdai.1	. . 3 |- F/ x ph
2		reximdai.2	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	1, 2	ralrimi 2864	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
4		rexim 2929	. 2 |- ( A. x e. A ( ps -> ch ) -> ( E. x e. A ps -> E. x e. A ch ) )
5	3, 4	syl 16	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   F/wnf 1599   e. wcel 1767   A.wral 2814   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820

This theorem is referenced by:  reximdvaiOLD  2936  tz7.49  7110  hsmexlem2  8807  indexdom  29856  filbcmb  29862  upbdrech  31110  infrglb  31168  limcperiod  31198  limsupre  31211  0ellimcdiv  31219  cncfshift  31240  cncfperiod  31245  ioodvbdlimc1lem1  31289  stoweidlem31  31359  stoweidlem34  31362  fourierdlem45  31480  fourierdlem73  31508  2reurex  31681  cdlemefr29exN  35216