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  4493  isoselem  5863  isosolem  5867  findcard  6944  nnsub  9021  supinfneg  9660  infsupneg  9661  ublbneg  9678  expnlbnd2  10736  cau3lem  11258  climshftlemg  11445  subcn2  11454  serf0  11495  sqrt2irr  12300  pclemub  12425  prmpwdvds  12493  grpinveu  13110  dfgrp3mlem  13170  issubg4m  13263  tgcn  14376  tgcnp  14377  lmconst  14384  cnntr  14393  lmss  14414  txdis  14445  txlm  14447  blbas  14601  metss  14662  metcnp3  14679  iswomni0  15541