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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralxfrd  4610  isoselem  6029  isosolem  6033  findcard  7196  nnsub  9352  supinfneg  10011  infsupneg  10012  ublbneg  10029  expnlbnd2  11124  hashfibc  11305  cau3lem  11903  climshftlemg  12093  subcn2  12102  serf0  12143  sqrt2irr  12966  pclemub  13095  prmpwdvds  13163  grpinveu  13902  dfgrp3mlem  13962  issubg4m  14055  tgcn  15434  tgcnp  15435  lmconst  15442  cnntr  15451  lmss  15472  txdis  15503  txlm  15505  blbas  15659  metss  15720  metcnp3  15737  iswomni0  17308