Theorem ralrimdva 2557

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralxfrd  4464  isoselem  5823  isosolem  5827  findcard  6890  nnsub  8960  supinfneg  9597  infsupneg  9598  ublbneg  9615  expnlbnd2  10648  cau3lem  11125  climshftlemg  11312  subcn2  11321  serf0  11362  sqrt2irr  12164  pclemub  12289  prmpwdvds  12355  grpinveu  12916  dfgrp3mlem  12973  issubg4m  13058  tgcn  13793  tgcnp  13794  lmconst  13801  cnntr  13810  lmss  13831  txdis  13862  txlm  13864  blbas  14018  metss  14079  metcnp3  14096  iswomni0  14884