Theorem ralrimdva 2555

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)

Hypothesis

Ref	Expression
ralrimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

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

Distinct variable groups:   ph, x   ps, x

Allowed substitution hints:   ch( x)   A( x)

Proof of Theorem ralrimdva

Step	Hyp	Ref	Expression
1		ralrimdva.1	. . . 4 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 115	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ps -> ( x e. A -> ch ) ) )
4	3	ralrimdv 2554	1 |- ( ph -> ( ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2146   A.wral 2453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1445  ax-gen 1447  ax-4 1508  ax-17 1524

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-ral 2458

This theorem is referenced by:  ralxfrd  4456  isoselem  5811  isosolem  5815  findcard  6878  nnsub  8931  supinfneg  9568  infsupneg  9569  ublbneg  9586  expnlbnd2  10615  cau3lem  11091  climshftlemg  11278  subcn2  11287  serf0  11328  sqrt2irr  12129  pclemub  12254  prmpwdvds  12320  grpinveu  12782  dfgrp3mlem  12838  tgcn  13288  tgcnp  13289  lmconst  13296  cnntr  13305  lmss  13326  txdis  13357  txlm  13359  blbas  13513  metss  13574  metcnp3  13591  iswomni0  14369