Theorem ralrimdva 2577

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralxfrd  4498  isoselem  5870  isosolem  5874  findcard  6958  nnsub  9048  supinfneg  9688  infsupneg  9689  ublbneg  9706  expnlbnd2  10776  cau3lem  11298  climshftlemg  11486  subcn2  11495  serf0  11536  sqrt2irr  12357  pclemub  12483  prmpwdvds  12551  grpinveu  13242  dfgrp3mlem  13302  issubg4m  13401  tgcn  14552  tgcnp  14553  lmconst  14560  cnntr  14569  lmss  14590  txdis  14621  txlm  14623  blbas  14777  metss  14838  metcnp3  14855  iswomni0  15808