Theorem ralrimdva 2630

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 2629	1 |- ( ph -> ( ps -> A. x e. A ch ) )

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  ralxfrd  4603  isoselem  6016  isosolem  6020  findcard  7182  nnsub  9322  supinfneg  9974  infsupneg  9975  ublbneg  9992  expnlbnd2  11081  hashfibc  11261  cau3lem  11858  climshftlemg  12046  subcn2  12055  serf0  12096  sqrt2irr  12918  pclemub  13044  prmpwdvds  13112  grpinveu  13820  dfgrp3mlem  13880  issubg4m  13973  tgcn  15232  tgcnp  15233  lmconst  15240  cnntr  15249  lmss  15270  txdis  15301  txlm  15303  blbas  15457  metss  15518  metcnp3  15535  iswomni0  17006