Theorem ralimdva 2795

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 436	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	a2d 29	. 2 |- ( ph -> ( ( x e. A -> ps ) -> ( x e. A -> ch ) ) )
4	3	ralimdv2 2794	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1886   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757

This theorem depends on definitions:  df-bi 189  df-an 373  df-ral 2741

This theorem is referenced by:  ralimdv  2797  ralimdvva  2798  wereu2  4830  fveqressseq  6016  f1mpt  6160  isores3  6224  caofrss  6561  caoftrn  6563  sorpssuni  6577  sorpssint  6578  onint  6619  smogt  7083  fisupg  7816  ixpfi2  7869  fissuni  7876  indexfi  7879  fiinfg  8012  wemaplem2  8059  rankonidlem  8296  ac5num  8464  acni2  8474  acndom2  8482  alephle  8516  dfac5  8556  cfsmolem  8697  isf34lem7  8806  isf34lem6  8807  fin1a2s  8841  acncc  8867  ttukeylem6  8941  fpwwe2lem8  9059  gchina  9121  inar1  9197  tskord  9202  grudomon  9239  grur1a  9241  dedekind  9794  fimaxre  10548  uzwo  11219  xrsupsslem  11589  xrinfmsslem  11590  fsuppmapnn0fiub0  12202  rexanre  13402  rexuz3  13404  rexico  13409  cau3lem  13410  limsupval2  13533  limsupval2OLD  13534  rlim2lt  13554  rlim3  13555  lo1bdd2  13581  lo1bddrp  13582  o1lo1  13594  climrlim2  13604  2clim  13629  o1co  13643  rlimcn1  13645  rlimcn2  13647  climcn1  13648  climcn2  13649  subcn2  13651  o1of2  13669  rlimo1  13673  o1rlimmul  13675  lo1add  13683  lo1mul  13684  climsqz  13697  climsqz2  13698  rlimsqzlem  13705  lo1le  13708  climbdd  13728  caucvgrlem  13729  caucvgrlemOLD  13730  caucvgrlem2  13733  caurcvg2  13737  iseralt  13744  cvgcmp  13869  cvgcmpce  13871  gcdcllem1  14466  absproddvds  14580  coprmprod  14671  coprmproddvdslem  14672  pcfac  14837  pockthg  14843  infpnlem1  14847  prmreclem2  14854  prmreclem3  14855  vdwlem11  14934  vdwlem13  14936  vdwnnlem3  14940  isacs2  15552  acsfn1  15560  acsfn2  15562  catpropd  15607  drsdirfi  16176  ipodrsima  16404  isacs5  16411  mrelatglb  16423  mrelatlub  16425  isgrpinv  16709  issubg4  16829  gsmsymgreqlem2  17065  gexdvds  17228  gexcl3  17232  sylow2blem3  17267  cyggeninv  17511  gsummptnn0fz  17608  dprdff  17638  issubdrg  18026  mptcoe1fsupp  18801  cply1coe0bi  18887  gsummoncoe1  18891  cygznlem3  19133  scmatdmat  19533  mdetdiagid  19618  mdetunilem9  19638  cpmatmcllem  19735  m2cpminvid2lem  19771  decpmatmulsumfsupp  19790  pmatcollpw1lem1  19791  pmatcollpw2lem  19794  pmatcollpwfi  19799  pm2mpf1  19816  mptcoe1matfsupp  19819  mp2pm2mplem4  19826  pm2mpmhmlem1  19835  pm2mp  19842  chpdmat  19858  chpscmat  19859  cpmidpmatlem3  19889  cayhamlem4  19905  neiptopnei  20141  cncnp  20289  isnrm2  20367  isreg2  20386  2ndcdisj  20464  islly2  20492  dislly  20505  kgen2ss  20563  ptbasfi  20589  ptclsg  20623  prdstopn  20636  txtube  20648  txlm  20656  isr0  20745  filuni  20893  alexsubALTlem3  21057  ptcmplem3  21062  ptcmplem4  21063  tsmsxplem1  21160  prdsmet  21378  metequiv2  21518  metcnpi3  21554  nmoleub  21729  nmoleubOLD  21745  rescncf  21922  cncfco  21932  evth  21980  lebnumlem3  21984  lebnumlem3OLD  21987  xlebnum  21989  nmoleub2lem2  22123  nmhmcn  22127  lmmcvg  22224  cmetcaulem  22251  caubl  22270  bcth3  22292  ovollb2lem  22434  ovoliunlem2  22449  ovolicc2lem3  22465  ovolicc2lem4OLD  22466  ovolicc2lem4  22467  nulmbl2  22483  volsup  22502  ioombl1lem4  22507  dyadmax  22549  vitalilem2  22560  vitalilem5  22563  mbfi1flimlem  22673  itg2seq  22693  itg2addlem  22709  itgcn  22793  limciun  22842  rolle  22935  dvfsumrlim  22976  itgsubst  22994  aannenlem1  23277  aalioulem3  23283  ulmcaulem  23342  ulmcau  23343  ulmss  23345  ulmbdd  23346  ulmcn  23347  ulmdvlem3  23350  mtest  23352  iblulm  23355  itgulm  23356  rlimcnp  23884  xrlimcnp  23887  rlimcxp  23892  o1cxp  23893  amgm  23909  lgambdd  23955  ftalem2  23991  isppw2  24035  mumullem2  24100  2sqlem6  24290  chtppilimlem2  24305  chtppilim  24306  pntrsumbnd2  24398  pntlem3  24440  isperp2  24753  axeuclidlem  24985  axeuclid  24986  cusgrares  25193  edgwlk  25252  usgrwlknloop  25286  redwlk  25329  cusconngra  25397  wlkiswwlk1  25411  wlkiswwlk2lem4  25415  usg2wlkeq  25429  wwlknred  25444  wwlkm1edg  25456  clwlkisclwwlklem2a  25506  clwlkisclwwlklem1  25508  usgravd00  25640  cusgraisrusgra  25659  rusgraprop2  25663  rusgraprop3  25664  frisusgranb  25718  2pthfrgrarn  25730  2pthfrgrarn2  25731  2pthfrgra  25732  3cyclfrgra  25736  frgrancvvdeq  25763  frgrancvvdgeq  25764  nmoub3i  26407  ubthlem1  26505  ubthlem3  26507  ocsh  26929  chintcli  26977  chscllem2  27284  nmopub2tALT  27555  nmfnleub2  27572  lnconi  27679  riesz1  27711  rnbra  27753  leopadd  27778  leopmuli  27779  leoptr  27783  dmdbr3  27951  dmdbr4  27952  dmdbr5  27954  mdsl0  27956  mdsymlem6  28054  cdj1i  28079  acunirnmpt  28254  xrge0infss  28333  xrge0infssOLD  28334  cmppcmp  28678  lmxrge0  28751  cvmlift2lem12  30030  opnrebl2  30970  neibastop1  31008  neibastop2lem  31009  neibastop3  31011  finixpnum  31923  ptrecube  31933  poimirlem26  31959  poimirlem27  31960  poimirlem29  31962  poimirlem30  31963  poimir  31966  heicant  31968  itg2addnclem  31986  itg2addnclem3  31988  itg2addnc  31989  filbcmb  32060  nninfnub  32073  geomcau  32081  sstotbnd2  32099  isbndx  32107  prdsbnd  32118  heibor1lem  32134  heiborlem1  32136  heibor  32146  rrncmslem  32157  intidl  32255  pclclN  33450  lauteq  33654  ltrnid  33694  mapdh9a  35352  elrfirn2  35532  isnacs3  35546  rencldnfilem  35657  kelac1  35915  acsfn1p  36059  cvgdvgrat  36656  neglimc  37722  stoweidlem7  37861  fourierdlem73  38037  sge0isum  38263  iccpartres  38726  uhgrnbgr0nb  39405  cusgrrusgr  39580  rusgrpropnb  39582  rusgrpropedg  39583  rusgrpropadjvtx  39584  upgrewlkle2  39608  1wlkvtxiedg  39620  wlk1wlk  39632  upgr1wlkwlk  39633  upgr1wlkvtxedg  39637  copisnmnd  39796  2zrngnmlid2  39938  ply1mulgsumlem1  40165  ply1mulgsumlem3  40167  ply1mulgsumlem4  40168  snlindsntor  40251