Theorem ralrimdva 2546

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 114	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ps -> ( x e. A -> ch ) ) )
4	3	ralrimdv 2545	1 |- ( ph -> ( ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2136   A.wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralxfrd  4440  isoselem  5788  isosolem  5792  findcard  6854  nnsub  8896  supinfneg  9533  infsupneg  9534  ublbneg  9551  expnlbnd2  10580  cau3lem  11056  climshftlemg  11243  subcn2  11252  serf0  11293  sqrt2irr  12094  pclemub  12219  prmpwdvds  12285  tgcn  12858  tgcnp  12859  lmconst  12866  cnntr  12875  lmss  12896  txdis  12927  txlm  12929  blbas  13083  metss  13144  metcnp3  13161  iswomni0  13940