Theorem ralrimdva 2624

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralxfrd  4588  isoselem  5999  isosolem  6003  findcard  7158  nnsub  9293  supinfneg  9945  infsupneg  9946  ublbneg  9963  expnlbnd2  11052  hashfibc  11232  cau3lem  11824  climshftlemg  12012  subcn2  12021  serf0  12062  sqrt2irr  12884  pclemub  13010  prmpwdvds  13078  grpinveu  13793  dfgrp3mlem  13853  issubg4m  13946  tgcn  15199  tgcnp  15200  lmconst  15207  cnntr  15216  lmss  15237  txdis  15268  txlm  15270  blbas  15424  metss  15485  metcnp3  15502  iswomni0  16962