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  4585  isoselem  5995  isosolem  5999  findcard  7147  nnsub  9278  supinfneg  9930  infsupneg  9931  ublbneg  9948  expnlbnd2  11031  hashfibc  11211  cau3lem  11803  climshftlemg  11991  subcn2  12000  serf0  12041  sqrt2irr  12863  pclemub  12989  prmpwdvds  13057  grpinveu  13768  dfgrp3mlem  13828  issubg4m  13927  tgcn  15090  tgcnp  15091  lmconst  15098  cnntr  15107  lmss  15128  txdis  15159  txlm  15161  blbas  15315  metss  15376  metcnp3  15393  iswomni0  16853