Theorem ralrimdva 2512

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 114	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ps -> ( x e. A -> ch ) ) )
4	3	ralrimdv 2511	1 |- ( ph -> ( ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1480   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  ralxfrd  4383  isoselem  5721  isosolem  5725  findcard  6782  nnsub  8759  supinfneg  9390  infsupneg  9391  ublbneg  9405  expnlbnd2  10417  cau3lem  10886  climshftlemg  11071  subcn2  11080  serf0  11121  sqrt2irr  11840  tgcn  12377  tgcnp  12378  lmconst  12385  cnntr  12394  lmss  12415  txdis  12446  txlm  12448  blbas  12602  metss  12663  metcnp3  12680