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  9343  supinfneg  9995  infsupneg  9996  ublbneg  10013  expnlbnd2  11103  hashfibc  11283  cau3lem  11880  climshftlemg  12068  subcn2  12077  serf0  12118  sqrt2irr  12940  pclemub  13066  prmpwdvds  13134  grpinveu  13843  dfgrp3mlem  13903  issubg4m  13996  tgcn  15309  tgcnp  15310  lmconst  15317  cnntr  15326  lmss  15347  txdis  15378  txlm  15380  blbas  15534  metss  15595  metcnp3  15612  iswomni0  17101