Theorem ralrimdva 2588

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  ralxfrd  4527  isoselem  5912  isosolem  5916  findcard  7011  nnsub  9110  supinfneg  9751  infsupneg  9752  ublbneg  9769  expnlbnd2  10847  cau3lem  11540  climshftlemg  11728  subcn2  11737  serf0  11778  sqrt2irr  12599  pclemub  12725  prmpwdvds  12793  grpinveu  13485  dfgrp3mlem  13545  issubg4m  13644  tgcn  14795  tgcnp  14796  lmconst  14803  cnntr  14812  lmss  14833  txdis  14864  txlm  14866  blbas  15020  metss  15081  metcnp3  15098  iswomni0  16192