Theorem ralimdva 2831

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

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1867   A.wral 2773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2778

This theorem is referenced by:  ralimdv  2833  ralimdvva  2834  wereu2  4842  fveqressseq  6024  f1mpt  6168  isores3  6232  caofrss  6569  caoftrn  6571  sorpssuni  6585  sorpssint  6586  onint  6627  smogt  7085  fisupg  7816  ixpfi2  7869  fissuni  7876  indexfi  7879  wemaplem2  8053  rankonidlem  8289  ac5num  8456  acni2  8466  acndom2  8474  alephle  8508  dfac5  8548  cfsmolem  8689  isf34lem7  8798  isf34lem6  8799  fin1a2s  8833  acncc  8859  ttukeylem6  8933  fpwwe2lem8  9051  gchina  9113  inar1  9189  tskord  9194  grudomon  9231  grur1a  9233  dedekind  9786  fimaxre  10540  uzwo  11211  xrsupsslem  11581  xrinfmsslem  11582  fsuppmapnn0fiub0  12191  rexanre  13377  rexuz3  13379  rexico  13384  cau3lem  13385  limsupval2  13507  limsupval2OLD  13508  rlim2lt  13528  rlim3  13529  lo1bdd2  13555  lo1bddrp  13556  o1lo1  13568  climrlim2  13578  2clim  13603  o1co  13617  rlimcn1  13619  rlimcn2  13621  climcn1  13622  climcn2  13623  subcn2  13625  o1of2  13643  rlimo1  13647  o1rlimmul  13649  lo1add  13657  lo1mul  13658  climsqz  13671  climsqz2  13672  rlimsqzlem  13679  lo1le  13682  climbdd  13702  caucvgrlem  13703  caucvgrlemOLD  13704  caucvgrlem2  13707  caurcvg2  13711  iseralt  13718  cvgcmp  13843  cvgcmpce  13845  gcdcllem1  14436  absproddvds  14547  coprmprod  14638  coprmproddvdslem  14639  pcfac  14796  pockthg  14802  infpnlem1  14806  prmreclem2  14813  prmreclem3  14814  vdwlem11  14893  vdwlem13  14895  vdwnnlem3  14899  isacs2  15503  acsfn1  15511  acsfn2  15513  catpropd  15558  drsdirfi  16127  ipodrsima  16355  isacs5  16362  mrelatglb  16374  mrelatlub  16376  isgrpinv  16660  issubg4  16780  gsmsymgreqlem2  17016  gexdvds  17164  gexcl3  17167  sylow2blem3  17202  cyggeninv  17446  gsummptnn0fz  17543  dprdff  17573  issubdrg  17961  mptcoe1fsupp  18736  cply1coe0bi  18822  gsummoncoe1  18826  cygznlem3  19064  scmatdmat  19464  mdetdiagid  19549  mdetunilem9  19569  cpmatmcllem  19666  m2cpminvid2lem  19702  decpmatmulsumfsupp  19721  pmatcollpw1lem1  19722  pmatcollpw2lem  19725  pmatcollpwfi  19730  pm2mpf1  19747  mptcoe1matfsupp  19750  mp2pm2mplem4  19757  pm2mpmhmlem1  19766  pm2mp  19773  chpdmat  19789  chpscmat  19790  cpmidpmatlem3  19820  cayhamlem4  19836  neiptopnei  20072  cncnp  20220  isnrm2  20298  isreg2  20317  2ndcdisj  20395  islly2  20423  dislly  20436  kgen2ss  20494  ptbasfi  20520  ptclsg  20554  prdstopn  20567  txtube  20579  txlm  20587  isr0  20676  filuni  20824  alexsubALTlem3  20988  ptcmplem3  20993  ptcmplem4  20994  tsmsxplem1  21091  prdsmet  21309  metequiv2  21449  metcnpi3  21485  nmoleub  21656  rescncf  21818  cncfco  21828  evth  21876  lebnumlem3  21880  xlebnum  21882  nmoleub2lem2  22016  nmhmcn  22020  lmmcvg  22117  cmetcaulem  22144  caubl  22163  bcth3  22185  ovollb2lem  22315  ovoliunlem2  22330  ovolicc2lem3  22346  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  nulmbl2  22364  volsup  22383  ioombl1lem4  22388  dyadmax  22430  vitalilem2  22441  vitalilem5  22444  mbfi1flimlem  22554  itg2seq  22574  itg2addlem  22590  itgcn  22674  limciun  22723  rolle  22816  dvfsumrlim  22857  itgsubst  22875  aannenlem1  23146  aalioulem3  23152  ulmcaulem  23211  ulmcau  23212  ulmss  23214  ulmbdd  23215  ulmcn  23216  ulmdvlem3  23219  mtest  23221  iblulm  23224  itgulm  23225  rlimcnp  23753  xrlimcnp  23756  rlimcxp  23761  o1cxp  23762  amgm  23778  lgambdd  23824  ftalem2  23860  isppw2  23902  mumullem2  23967  2sqlem6  24157  chtppilimlem2  24172  chtppilim  24173  pntrsumbnd2  24265  pntlem3  24307  isperp2  24614  axeuclidlem  24835  axeuclid  24836  cusgrares  25042  edgwlk  25101  usgrnloop  25135  redwlk  25178  cusconngra  25246  wlkiswwlk1  25260  wlkiswwlk2lem4  25264  usg2wlkeq  25278  wwlknred  25293  wwlkm1edg  25305  clwlkisclwwlklem2a  25355  clwlkisclwwlklem1  25357  usgravd00  25489  cusgraisrusgra  25508  rusgraprop2  25512  rusgraprop3  25513  frisusgranb  25567  2pthfrgrarn  25579  2pthfrgrarn2  25580  2pthfrgra  25581  3cyclfrgra  25585  frgrancvvdeq  25612  frgrancvvdgeq  25613  nmoub3i  26256  ubthlem1  26354  ubthlem3  26356  ocsh  26768  chintcli  26816  chscllem2  27123  nmopub2tALT  27394  nmfnleub2  27411  lnconi  27518  riesz1  27550  rnbra  27592  leopadd  27617  leopmuli  27618  leoptr  27622  dmdbr3  27790  dmdbr4  27791  dmdbr5  27793  mdsl0  27795  mdsymlem6  27893  cdj1i  27918  acunirnmpt  28098  xrge0infss  28178  cmppcmp  28521  lmxrge0  28594  cvmlift2lem12  29822  opnrebl2  30759  neibastop1  30797  neibastop2lem  30798  neibastop3  30800  finixpnum  31634  ptrecube  31644  poimirlem26  31670  poimirlem27  31671  poimirlem29  31673  poimirlem30  31674  poimir  31677  heicant  31679  itg2addnclem  31697  itg2addnclem3  31699  itg2addnc  31700  filbcmb  31771  nninfnub  31784  geomcau  31792  sstotbnd2  31810  isbndx  31818  prdsbnd  31829  heibor1lem  31845  heiborlem1  31847  heibor  31857  rrncmslem  31868  intidl  31966  pclclN  33165  lauteq  33369  ltrnid  33409  mapdh9a  35067  elrfirn2  35247  isnacs3  35261  rencldnfilem  35372  kelac1  35631  acsfn1p  35768  cvgdvgrat  36303  neglimc  37304  stoweidlem7  37440  fourierdlem73  37615  iccpartres  38135  copisnmnd  38580  2zrngnmlid2  38722  ply1mulgsumlem1  38951  ply1mulgsumlem3  38953  ply1mulgsumlem4  38954  snlindsntor  39037