Theorem ralrimdva 2574

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralxfrd  4494  isoselem  5864  isosolem  5868  findcard  6946  nnsub  9023  supinfneg  9663  infsupneg  9664  ublbneg  9681  expnlbnd2  10739  cau3lem  11261  climshftlemg  11448  subcn2  11457  serf0  11498  sqrt2irr  12303  pclemub  12428  prmpwdvds  12496  grpinveu  13113  dfgrp3mlem  13173  issubg4m  13266  tgcn  14387  tgcnp  14388  lmconst  14395  cnntr  14404  lmss  14425  txdis  14456  txlm  14458  blbas  14612  metss  14673  metcnp3  14690  iswomni0  15611