Theorem ralimdva 2962

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 5-Dec-2019.)

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		ralimdva.1	. . . 4 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 450	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	a2d 29	. 2 |- ( ph -> ( ( x e. A -> ps ) -> ( x e. A -> ch ) ) )
4	3	ralimdv2 2961	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  ralimdv  2963  ralimdvva  2964  wereu2  5111  fveqressseq  6355  f1mpt  6518  isores3  6585  caofrss  6930  caoftrn  6932  sorpssuni  6946  sorpssint  6947  onint  6995  smogt  7464  fisupg  8208  ixpfi2  8264  fissuni  8271  indexfi  8274  fiinfg  8405  wemaplem2  8452  rankonidlem  8691  ac5num  8859  acni2  8869  acndom2  8877  alephle  8911  dfac5  8951  cfsmolem  9092  isf34lem7  9201  isf34lem6  9202  fin1a2s  9236  acncc  9262  ttukeylem6  9336  fpwwe2lem8  9459  gchina  9521  inar1  9597  tskord  9602  grudomon  9639  grur1a  9641  dedekind  10200  fimaxre  10968  uzwo  11751  xrsupsslem  12137  xrinfmsslem  12138  fsuppmapnn0fiub0  12793  rexanre  14086  rexuz3  14088  rexico  14093  cau3lem  14094  limsupval2  14211  rlim2lt  14228  rlim3  14229  lo1bdd2  14255  lo1bddrp  14256  o1lo1  14268  climrlim2  14278  2clim  14303  o1co  14317  rlimcn1  14319  rlimcn2  14321  climcn1  14322  climcn2  14323  subcn2  14325  o1of2  14343  rlimo1  14347  o1rlimmul  14349  lo1add  14357  lo1mul  14358  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  lo1le  14382  climbdd  14402  caucvgrlem  14403  caucvgrlem2  14405  caurcvg2  14408  iseralt  14415  cvgcmp  14548  cvgcmpce  14550  gcdcllem1  15221  absproddvds  15330  coprmprod  15375  coprmproddvdslem  15376  pcfac  15603  pockthg  15610  infpnlem1  15614  prmreclem2  15621  prmreclem3  15622  vdwlem11  15695  vdwlem13  15697  vdwnnlem3  15701  isacs2  16314  acsfn1  16322  acsfn2  16324  catpropd  16369  drsdirfi  16938  ipodrsima  17165  isacs5  17172  mrelatglb  17184  mrelatlub  17186  isgrpinv  17472  dfgrp3e  17515  issubg4  17613  gsmsymgreqlem2  17851  gexdvds  17999  gexcl3  18002  sylow2blem3  18037  cyggeninv  18285  gsummptnn0fz  18382  dprdff  18411  issubdrg  18805  mptcoe1fsupp  19585  cply1coe0bi  19670  gsummoncoe1  19674  cygznlem3  19918  scmatdmat  20321  mdetdiagid  20406  mdetunilem9  20426  cpmatmcllem  20523  m2cpminvid2lem  20559  decpmatmulsumfsupp  20578  pmatcollpw1lem1  20579  pmatcollpw2lem  20582  pmatcollpwfi  20587  pm2mpf1  20604  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  pm2mpmhmlem1  20623  pm2mp  20630  chpdmat  20646  chpscmat  20647  cpmidpmatlem3  20677  cayhamlem4  20693  neiptopnei  20936  cncnp  21084  isnrm2  21162  isreg2  21181  2ndcdisj  21259  islly2  21287  dislly  21300  kgen2ss  21358  ptbasfi  21384  ptclsg  21418  prdstopn  21431  txtube  21443  txlm  21451  isr0  21540  filuni  21689  alexsubALTlem3  21853  ptcmplem3  21858  ptcmplem4  21859  tsmsxplem1  21956  prdsmet  22175  metequiv2  22315  metcnpi3  22351  nmoleub  22535  rescncf  22700  cncfco  22710  evth  22758  lebnumlem3  22762  xlebnum  22764  nmoleub2lem2  22916  nmhmcn  22920  lmmcvg  23059  cmetcaulem  23086  caubl  23106  bcth3  23128  ovollb2lem  23256  ovoliunlem2  23271  ovolicc2lem3  23287  ovolicc2lem4  23288  nulmbl2  23304  volsup  23324  ioombl1lem4  23329  dyadmax  23366  vitalilem2  23378  vitalilem5  23381  mbfi1flimlem  23489  itg2seq  23509  itg2addlem  23525  itgcn  23609  limciun  23658  rolle  23753  dvfsumrlim  23794  itgsubst  23812  aannenlem1  24083  aalioulem3  24089  ulmcaulem  24148  ulmcau  24149  ulmss  24151  ulmbdd  24152  ulmcn  24153  ulmdvlem3  24156  mtest  24158  iblulm  24161  itgulm  24162  rlimcnp  24692  xrlimcnp  24695  rlimcxp  24700  o1cxp  24701  amgm  24717  lgambdd  24763  ftalem2  24800  isppw2  24841  mumullem2  24906  2sqlem6  25148  chtppilimlem2  25163  chtppilim  25164  pntrsumbnd2  25256  pntlem3  25298  isperp2  25610  axeuclidlem  25842  axeuclid  25843  uhgrnbgr0nb  26250  vtxdginducedm1fi  26440  cusgrrusgr  26477  rusgrpropnb  26479  rusgrpropedg  26480  rusgrpropadjvtx  26481  upgrewlkle2  26502  wlkvtxiedg  26520  upgrwlkvtxedg  26541  uspgr2wlkeq  26542  redwlk  26569  wlkdlem2  26580  lfgrwlkprop  26584  2pthnloop  26627  upgr2pthnlp  26628  pthdlem1  26662  pthdlem2lem  26663  wlkiswwlks1  26753  wlkiswwlks2lem4  26758  wwlksm1edg  26767  wwlksnred  26787  clwlkclwwlklem2a  26899  clwlkclwwlklem2  26901  cusconngr  27051  eucrctshift  27103  2pthfrgr  27148  3cyclfrgr  27152  nmoub3i  27628  ubthlem1  27726  ubthlem3  27728  ocsh  28142  chintcli  28190  chscllem2  28497  nmopub2tALT  28768  nmfnleub2  28785  lnconi  28892  riesz1  28924  rnbra  28966  leopadd  28991  leopmuli  28992  leoptr  28996  dmdbr3  29164  dmdbr4  29165  dmdbr5  29167  mdsl0  29169  mdsymlem6  29267  cdj1i  29292  acunirnmpt  29459  xrge0infss  29525  cmppcmp  29925  lmxrge0  29998  ftc2re  30676  cvmlift2lem12  31296  nosupbnd1lem5  31858  noetalem3  31865  opnrebl2  32316  neibastop1  32354  neibastop2lem  32355  neibastop3  32357  finixpnum  33394  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  ptrecube  33409  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimir  33442  heicant  33444  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  filbcmb  33535  nninfnub  33547  geomcau  33555  sstotbnd2  33573  isbndx  33581  prdsbnd  33592  heibor1lem  33608  heiborlem1  33610  heibor  33620  rrncmslem  33631  intidl  33828  pclclN  35177  lauteq  35381  ltrnid  35421  mapdh9a  37079  elrfirn2  37259  isnacs3  37273  rencldnfilem  37384  kelac1  37633  acsfn1p  37769  neik0pk1imk0  38345  cvgdvgrat  38512  neglimc  39879  limsupub  39936  limsuppnflem  39942  limsupre3lem  39964  limsupvaluz2  39970  supcnvlimsup  39972  climuzlem  39975  liminfval2  40000  limsupgtlem  40009  liminflelimsupuz  40017  liminflimsupclim  40039  xlimmnfv  40060  xlimpnfv  40064  stoweidlem7  40224  fourierdlem73  40396  sge0isum  40644  preimageiingt  40930  preimaleiinlt  40931  smflimlem3  40981  smflimlem4  40982  iccpartres  41354  upwlkwlk  41720  upgrwlkupwlk  41721  copisnmnd  41809  2zrngnmlid2  41951  ply1mulgsumlem1  42174  ply1mulgsumlem3  42176  ply1mulgsumlem4  42177  snlindsntor  42260