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  4608  isoselem  6026  isosolem  6030  findcard  7192  nnsub  9346  supinfneg  10005  infsupneg  10006  ublbneg  10023  expnlbnd2  11118  hashfibc  11299  cau3lem  11897  climshftlemg  12087  subcn2  12096  serf0  12137  sqrt2irr  12960  pclemub  13089  prmpwdvds  13157  grpinveu  13896  dfgrp3mlem  13956  issubg4m  14049  tgcn  15400  tgcnp  15401  lmconst  15408  cnntr  15417  lmss  15438  txdis  15469  txlm  15471  blbas  15625  metss  15686  metcnp3  15703  iswomni0  17268