Theorem reximdai 2856

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 2788	. 2 |- ( ph -> A. x e. A ( ps -> ch ) )
4		rexim 2852	. 2 |- ( A. x e. A ( ps -> ch ) -> ( E. x e. A ps -> E. x e. A ch ) )
5	3, 4	syl 17	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   F/wnf 1667   e. wcel 1887   A.wral 2737   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742  df-rex 2743

This theorem is referenced by:  reximdvaiOLD  2860  tz7.49  7162  hsmexlem2  8857  acunirnmpt2  28262  acunirnmpt2f  28263  locfinreflem  28667  cmpcref  28677  indexdom  32061  filbcmb  32067  cdlemefr29exN  33969  disjrnmpt2  37463  fompt  37467  disjinfi  37468  supxrge  37561  suplesup  37562  infrglbOLD  37669  limsupre  37721  limsupreOLD  37722  stoweidlem31  37892  stoweidlem34  37895  fourierdlem73  38043  sge0pnffigt  38238  sge0ltfirp  38242  iundjiun  38298  ovnlerp  38384  2reurex  38602