Theorem ralrimdva 2610

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralxfrd  4553  isoselem  5944  isosolem  5948  findcard  7050  nnsub  9149  supinfneg  9790  infsupneg  9791  ublbneg  9808  expnlbnd2  10887  cau3lem  11625  climshftlemg  11813  subcn2  11822  serf0  11863  sqrt2irr  12684  pclemub  12810  prmpwdvds  12878  grpinveu  13571  dfgrp3mlem  13631  issubg4m  13730  tgcn  14882  tgcnp  14883  lmconst  14890  cnntr  14899  lmss  14920  txdis  14951  txlm  14953  blbas  15107  metss  15168  metcnp3  15185  iswomni0  16419