Theorem ralimdva 2622

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
ralimdva	|- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		nfv 1605	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2621	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 358   e. wcel 1685   A.wral 2544

This theorem is referenced by:  ralimdv  2623  wereu2  4389  onint  4585  f1mpt  5747  isores3  5794  caofrss  6072  caoftrn  6074  sorpssuni  6248  sorpssint  6249  smogt  6380  tfrlem1  6387  fisupg  7101  ixpfi2  7150  fissuni  7156  indexfi  7159  wemaplem2  7258  rankonidlem  7496  ac5num  7659  acni2  7669  acndom2  7677  alephle  7711  dfac5  7751  cfsmolem  7892  isf34lem7  8001  isf34lem6  8002  fin1a2s  8036  acncc  8062  ttukeylem6  8137  fpwwe2lem8  8255  gchina  8317  inar1  8393  tskord  8398  grudomon  8435  grur1a  8437  fimaxre  9697  uzwo  10277  uzwoOLD  10278  xrsupsslem  10621  xrinfmsslem  10622  rexanre  11826  rexuz3  11828  rexico  11833  cau3lem  11834  limsupval2  11950  rlim2lt  11967  rlim3  11968  lo1bdd2  11994  lo1bddrp  11995  o1lo1  12007  climrlim2  12017  2clim  12042  o1co  12056  rlimcn1  12058  rlimcn2  12060  climcn1  12061  climcn2  12062  subcn2  12064  o1of2  12082  rlimo1  12086  o1rlimmul  12088  lo1add  12096  lo1mul  12097  climsqz  12110  climsqz2  12111  rlimsqzlem  12118  lo1le  12121  caucvgrlem  12141  caucvgrlem2  12143  caurcvg2  12146  iseralt  12153  cvgcmp  12270  cvgcmpce  12272  gcdcllem1  12686  pcfac  12943  pockthg  12949  infpnlem1  12953  prmreclem2  12960  prmreclem3  12961  vdwlem11  13034  vdwlem13  13036  vdwnnlem3  13040  isacs2  13551  acsfn1  13559  acsfn2  13561  catpropd  13608  drsdirfi  14068  ipodrsima  14264  isacs5  14271  mrelatglb  14283  mrelatlub  14285  isgrpinv  14528  issubg4  14634  gexdvds  14891  gexcl3  14894  sylow2blem3  14929  cyggeninv  15166  dprdff  15243  issubdrg  15566  islmhm2  15791  cygznlem3  16519  cncnp  17005  isnrm2  17082  isreg2  17101  2ndcdisj  17178  islly2  17206  dislly  17219  kgen2ss  17246  ptbasfi  17272  ptclsg  17305  prdstopn  17318  txtube  17330  txlm  17338  isr0  17424  filuni  17576  alexsubALTlem3  17739  ptcmplem3  17744  ptcmplem4  17745  tgpt0  17797  tsmsxplem1  17831  prdsmet  17930  metequiv2  18052  metcnpi3  18088  isngp4  18129  nmoleub  18236  addcnlem  18364  rescncf  18397  cncfco  18407  evth  18453  lebnumlem3  18457  xlebnum  18459  nmoleub2lem2  18593  nmhmcn  18597  lmmcvg  18683  cmetcaulem  18710  caubl  18729  bcth3  18749  ovollb2lem  18843  ovoliunlem2  18858  ovolicc2lem3  18874  ovolicc2lem4  18875  nulmbl2  18890  volsup  18909  ioombl1lem4  18914  dyadmax  18949  vitalilem2  18960  vitalilem5  18963  mbfi1flimlem  19073  itg2seq  19093  itg2addlem  19109  itgcn  19193  limciun  19240  rolle  19333  c1lip3  19342  dvfsumrlim  19374  itgsubst  19392  aannenlem1  19704  aalioulem2  19709  aalioulem3  19710  aalioulem5  19712  aalioulem6  19713  aaliou  19714  ulmcaulem  19767  ulmcau  19768  ulmss  19770  ulmbdd  19771  ulmcn  19772  ulmdvlem3  19775  mtest  19777  iblulm  19779  itgulm  19780  rlimcnp  20256  xrlimcnp  20259  rlimcxp  20264  o1cxp  20265  amgm  20281  ftalem2  20307  isppw2  20349  mumullem2  20414  2sqlem6  20604  chtppilimlem2  20619  chtppilim  20620  pntrsumbnd2  20712  pntlem3  20754  nmoub3i  21345  ubthlem1  21443  ubthlem3  21445  ocsh  21858  chintcli  21906  chscllem2  22213  nmopub2tALT  22485  nmfnleub2  22502  lnconi  22609  riesz1  22641  rnbra  22683  leopadd  22708  leopmuli  22709  leoptr  22713  dmdbr3  22881  dmdbr4  22882  dmdbr5  22884  mdsl0  22886  mdsymlem6  22984  cdj1i  23009  cvmlift2lem12  23252  dedekind  23488  dedekindle  23489  axfelem8  23757  axeuclidlem  24000  axeuclid  24001  mgmlion  24748  intfmu2  24930  islimrs3  24992  islimrs4  24993  icmpmon  25227  bhp3  25588  opnrebl2  25647  neibastop1  25719  neibastop2lem  25720  neibastop3  25722  filbcmb  25843  nninfnub  25872  geomcau  25886  sstotbnd2  25909  isbndx  25917  equivbnd  25925  prdsbnd  25928  heibor1lem  25944  heiborlem1  25946  heibor  25956  rrncmslem  25967  ghomco  25984  intidl  26065  elrfirn2  26182  isnacs3  26196  rencldnfilem  26314  kelac1  26572  acsfn1p  26918  stoweidlem7  27167  pclclN  29359  lauteq  29563  ltrnid  29603  mapdh9a  31259

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716

This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2549