Theorem ralrimdva 2630

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralxfrd  4610  isoselem  6029  isosolem  6033  findcard  7198  nnsub  9352  supinfneg  10010  infsupneg  10011  ublbneg  10028  expnlbnd2  11123  hashfibc  11304  cau3lem  11902  climshftlemg  12092  subcn2  12101  serf0  12142  sqrt2irr  12965  pclemub  13094  prmpwdvds  13162  grpinveu  13901  dfgrp3mlem  13961  issubg4m  14054  tgcn  15451  tgcnp  15452  lmconst  15459  cnntr  15468  lmss  15489  txdis  15520  txlm  15522  blbas  15676  metss  15737  metcnp3  15754  iswomni0  17325