Theorem ralrimdva 2610

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralxfrd  4555  isoselem  5954  isosolem  5958  findcard  7068  nnsub  9170  supinfneg  9817  infsupneg  9818  ublbneg  9835  expnlbnd2  10915  cau3lem  11662  climshftlemg  11850  subcn2  11859  serf0  11900  sqrt2irr  12721  pclemub  12847  prmpwdvds  12915  grpinveu  13608  dfgrp3mlem  13668  issubg4m  13767  tgcn  14919  tgcnp  14920  lmconst  14927  cnntr  14936  lmss  14957  txdis  14988  txlm  14990  blbas  15144  metss  15205  metcnp3  15222  iswomni0  16565