Theorem ralimdva 2805

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 441	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	a2d 28	. 2 |- ( ph -> ( ( x e. A -> ps ) -> ( x e. A -> ch ) ) )
4	3	ralimdv2 2804	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 376   e. wcel 1904   A.wral 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-an 378  df-ral 2761

This theorem is referenced by:  ralimdv  2806  ralimdvva  2807  wereu2  4836  fveqressseq  6033  f1mpt  6180  isores3  6244  caofrss  6583  caoftrn  6585  sorpssuni  6599  sorpssint  6600  onint  6641  smogt  7104  fisupg  7837  ixpfi2  7890  fissuni  7897  indexfi  7900  fiinfg  8033  wemaplem2  8080  rankonidlem  8317  ac5num  8485  acni2  8495  acndom2  8503  alephle  8537  dfac5  8577  cfsmolem  8718  isf34lem7  8827  isf34lem6  8828  fin1a2s  8862  acncc  8888  ttukeylem6  8962  fpwwe2lem8  9080  gchina  9142  inar1  9218  tskord  9223  grudomon  9260  grur1a  9262  dedekind  9815  fimaxre  10573  uzwo  11245  xrsupsslem  11617  xrinfmsslem  11618  fsuppmapnn0fiub0  12243  rexanre  13486  rexuz3  13488  rexico  13493  cau3lem  13494  limsupval2  13617  limsupval2OLD  13618  rlim2lt  13638  rlim3  13639  lo1bdd2  13665  lo1bddrp  13666  o1lo1  13678  climrlim2  13688  2clim  13713  o1co  13727  rlimcn1  13729  rlimcn2  13731  climcn1  13732  climcn2  13733  subcn2  13735  o1of2  13753  rlimo1  13757  o1rlimmul  13759  lo1add  13767  lo1mul  13768  climsqz  13781  climsqz2  13782  rlimsqzlem  13789  lo1le  13792  climbdd  13812  caucvgrlem  13813  caucvgrlemOLD  13814  caucvgrlem2  13817  caurcvg2  13821  iseralt  13828  cvgcmp  13953  cvgcmpce  13955  gcdcllem1  14552  absproddvds  14666  coprmprod  14757  coprmproddvdslem  14758  pcfac  14923  pockthg  14929  infpnlem1  14933  prmreclem2  14940  prmreclem3  14941  vdwlem11  15020  vdwlem13  15022  vdwnnlem3  15026  isacs2  15637  acsfn1  15645  acsfn2  15647  catpropd  15692  drsdirfi  16261  ipodrsima  16489  isacs5  16496  mrelatglb  16508  mrelatlub  16510  isgrpinv  16794  issubg4  16914  gsmsymgreqlem2  17150  gexdvds  17313  gexcl3  17317  sylow2blem3  17352  cyggeninv  17596  gsummptnn0fz  17693  dprdff  17723  issubdrg  18111  mptcoe1fsupp  18885  cply1coe0bi  18971  gsummoncoe1  18975  cygznlem3  19217  scmatdmat  19617  mdetdiagid  19702  mdetunilem9  19722  cpmatmcllem  19819  m2cpminvid2lem  19855  decpmatmulsumfsupp  19874  pmatcollpw1lem1  19875  pmatcollpw2lem  19878  pmatcollpwfi  19883  pm2mpf1  19900  mptcoe1matfsupp  19903  mp2pm2mplem4  19910  pm2mpmhmlem1  19919  pm2mp  19926  chpdmat  19942  chpscmat  19943  cpmidpmatlem3  19973  cayhamlem4  19989  neiptopnei  20225  cncnp  20373  isnrm2  20451  isreg2  20470  2ndcdisj  20548  islly2  20576  dislly  20589  kgen2ss  20647  ptbasfi  20673  ptclsg  20707  prdstopn  20720  txtube  20732  txlm  20740  isr0  20829  filuni  20978  alexsubALTlem3  21142  ptcmplem3  21147  ptcmplem4  21148  tsmsxplem1  21245  prdsmet  21463  metequiv2  21603  metcnpi3  21639  nmoleub  21814  nmoleubOLD  21830  rescncf  22007  cncfco  22017  evth  22065  lebnumlem3  22069  lebnumlem3OLD  22072  xlebnum  22074  nmoleub2lem2  22208  nmhmcn  22212  lmmcvg  22309  cmetcaulem  22336  caubl  22355  bcth3  22377  ovollb2lem  22519  ovoliunlem2  22534  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  nulmbl2  22568  volsup  22588  ioombl1lem4  22593  dyadmax  22635  vitalilem2  22646  vitalilem5  22649  mbfi1flimlem  22759  itg2seq  22779  itg2addlem  22795  itgcn  22879  limciun  22928  rolle  23021  dvfsumrlim  23062  itgsubst  23080  aannenlem1  23363  aalioulem3  23369  ulmcaulem  23428  ulmcau  23429  ulmss  23431  ulmbdd  23432  ulmcn  23433  ulmdvlem3  23436  mtest  23438  iblulm  23441  itgulm  23442  rlimcnp  23970  xrlimcnp  23973  rlimcxp  23978  o1cxp  23979  amgm  23995  lgambdd  24041  ftalem2  24077  isppw2  24121  mumullem2  24186  2sqlem6  24376  chtppilimlem2  24391  chtppilim  24392  pntrsumbnd2  24484  pntlem3  24526  isperp2  24839  axeuclidlem  25071  axeuclid  25072  cusgrares  25279  edgwlk  25338  usgrwlknloop  25372  redwlk  25415  cusconngra  25483  wlkiswwlk1  25497  wlkiswwlk2lem4  25501  usg2wlkeq  25515  wwlknred  25530  wwlkm1edg  25542  clwlkisclwwlklem2a  25592  clwlkisclwwlklem1  25594  usgravd00  25726  cusgraisrusgra  25745  rusgraprop2  25749  rusgraprop3  25750  frisusgranb  25804  2pthfrgrarn  25816  2pthfrgrarn2  25817  2pthfrgra  25818  3cyclfrgra  25822  frgrancvvdeq  25849  frgrancvvdgeq  25850  nmoub3i  26495  ubthlem1  26593  ubthlem3  26595  ocsh  27017  chintcli  27065  chscllem2  27372  nmopub2tALT  27643  nmfnleub2  27660  lnconi  27767  riesz1  27799  rnbra  27841  leopadd  27866  leopmuli  27867  leoptr  27871  dmdbr3  28039  dmdbr4  28040  dmdbr5  28042  mdsl0  28044  mdsymlem6  28142  cdj1i  28167  acunirnmpt  28336  xrge0infss  28415  xrge0infssOLD  28416  cmppcmp  28759  lmxrge0  28832  cvmlift2lem12  30109  opnrebl2  31048  neibastop1  31086  neibastop2lem  31087  neibastop3  31089  finixpnum  31994  ptrecube  32004  poimirlem26  32030  poimirlem27  32031  poimirlem29  32033  poimirlem30  32034  poimir  32037  heicant  32039  itg2addnclem  32057  itg2addnclem3  32059  itg2addnc  32060  filbcmb  32131  nninfnub  32144  geomcau  32152  sstotbnd2  32170  isbndx  32178  prdsbnd  32189  heibor1lem  32205  heiborlem1  32207  heibor  32217  rrncmslem  32228  intidl  32326  pclclN  33527  lauteq  33731  ltrnid  33771  mapdh9a  35429  elrfirn2  35609  isnacs3  35623  rencldnfilem  35734  kelac1  35992  acsfn1p  36136  cvgdvgrat  36732  neglimc  37825  stoweidlem7  37979  fourierdlem73  38155  sge0isum  38383  iccpartres  38877  uhgrnbgr0nb  39586  cusgrrusgr  39786  rusgrpropnb  39788  rusgrpropedg  39789  rusgrpropadjvtx  39790  upgrewlkle2  39812  1wlkvtxiedg  39827  wlk1wlk  39841  upgr1wlkwlk  39842  upgr1wlkvtxedg  39847  red1wlk  39868  lfgrwlkprop  39879  1wlkdlem2  39883  2pthnloop  39924  upgr2pthnlp  39925  pthdlem1  39952  pthdlem2lem  39953  cusconngr  40105  eucrctshift  40155  copisnmnd  40317  2zrngnmlid2  40459  ply1mulgsumlem1  40686  ply1mulgsumlem3  40688  ply1mulgsumlem4  40689  snlindsntor  40772