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  4557  isoselem  5956  isosolem  5960  findcard  7070  nnsub  9172  supinfneg  9819  infsupneg  9820  ublbneg  9837  expnlbnd2  10917  cau3lem  11665  climshftlemg  11853  subcn2  11862  serf0  11903  sqrt2irr  12724  pclemub  12850  prmpwdvds  12918  grpinveu  13611  dfgrp3mlem  13671  issubg4m  13770  tgcn  14922  tgcnp  14923  lmconst  14930  cnntr  14939  lmss  14960  txdis  14991  txlm  14993  blbas  15147  metss  15208  metcnp3  15225  iswomni0  16591