Theorem ralrimdva 2586

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralxfrd  4510  isoselem  5891  isosolem  5895  findcard  6987  nnsub  9077  supinfneg  9718  infsupneg  9719  ublbneg  9736  expnlbnd2  10812  cau3lem  11458  climshftlemg  11646  subcn2  11655  serf0  11696  sqrt2irr  12517  pclemub  12643  prmpwdvds  12711  grpinveu  13403  dfgrp3mlem  13463  issubg4m  13562  tgcn  14713  tgcnp  14714  lmconst  14721  cnntr  14730  lmss  14751  txdis  14782  txlm  14784  blbas  14938  metss  14999  metcnp3  15016  iswomni0  16027