Theorem ralimdva 2872

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 434	. . 3 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	a2d 26	. 2 |- ( ph -> ( ( x e. A -> ps ) -> ( x e. A -> ch ) ) )
4	3	ralimdv2 2871	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819

This theorem is referenced by:  ralimdv  2874  ralimdvva  2875  wereu2  4876  f1mpt  6155  isores3  6217  caofrss  6555  caoftrn  6557  sorpssuni  6571  sorpssint  6572  onint  6608  smogt  7035  fisupg  7764  ixpfi2  7814  fissuni  7821  indexfi  7824  wemaplem2  7968  rankonidlem  8242  ac5num  8413  acni2  8423  acndom2  8431  alephle  8465  dfac5  8505  cfsmolem  8646  isf34lem7  8755  isf34lem6  8756  fin1a2s  8790  acncc  8816  ttukeylem6  8890  fpwwe2lem8  9011  gchina  9073  inar1  9149  tskord  9154  grudomon  9191  grur1a  9193  dedekind  9739  dedekindle  9740  fimaxre  10486  uzwo  11140  uzwoOLD  11141  xrsupsslem  11494  xrinfmsslem  11495  fsuppmapnn0fiub0  12062  rexanre  13135  rexuz3  13137  rexico  13142  cau3lem  13143  limsupval2  13259  rlim2lt  13276  rlim3  13277  lo1bdd2  13303  lo1bddrp  13304  o1lo1  13316  climrlim2  13326  2clim  13351  o1co  13365  rlimcn1  13367  rlimcn2  13369  climcn1  13370  climcn2  13371  subcn2  13373  o1of2  13391  rlimo1  13395  o1rlimmul  13397  lo1add  13405  lo1mul  13406  climsqz  13419  climsqz2  13420  rlimsqzlem  13427  lo1le  13430  climbdd  13450  caucvgrlem  13451  caucvgrlem2  13453  caurcvg2  13456  iseralt  13463  cvgcmp  13586  cvgcmpce  13588  gcdcllem1  14001  pcfac  14270  pockthg  14276  infpnlem1  14280  prmreclem2  14287  prmreclem3  14288  vdwlem11  14361  vdwlem13  14363  vdwnnlem3  14367  isacs2  14901  acsfn1  14909  acsfn2  14911  catpropd  14958  drsdirfi  15418  ipodrsima  15645  isacs5  15652  mrelatglb  15664  mrelatlub  15666  isgrpinv  15898  issubg4  16012  gsmsymgreqlem2  16248  gexdvds  16397  gexcl3  16400  sylow2blem3  16435  cyggeninv  16674  gsummptnn0fz  16802  dprdff  16833  dprdffOLD  16839  issubdrg  17234  islmhm2  17464  mptcoe1fsupp  18023  cply1coe0bi  18110  gsummoncoe1  18114  cygznlem3  18372  scmatdmat  18781  mdetdiagid  18866  mdetunilem9  18886  cpmatmcllem  18983  m2cpminvid2lem  19019  decpmatmulsumfsupp  19038  pmatcollpw1lem1  19039  pmatcollpw2lem  19042  pmatcollpwfi  19047  pm2mpf1  19064  mptcoe1matfsupp  19067  mp2pm2mplem4  19074  pm2mpmhmlem1  19083  pm2mp  19090  chpdmat  19106  chpscmat  19107  cpmidpmatlem3  19137  cayhamlem4  19153  neiptopnei  19396  cncnp  19544  isnrm2  19622  isreg2  19641  2ndcdisj  19720  islly2  19748  dislly  19761  kgen2ss  19788  ptbasfi  19814  ptclsg  19848  prdstopn  19861  txtube  19873  txlm  19881  isr0  19970  filuni  20118  alexsubALTlem3  20281  ptcmplem3  20286  ptcmplem4  20287  tgpt0  20349  tsmsxplem1  20387  prdsmet  20605  metequiv2  20745  metcnpi3  20781  isngp4  20863  nmoleub  20970  addcnlem  21100  rescncf  21133  cncfco  21143  evth  21191  lebnumlem3  21195  xlebnum  21197  nmoleub2lem2  21331  nmhmcn  21335  lmmcvg  21432  cmetcaulem  21459  caubl  21478  bcth3  21502  ovollb2lem  21631  ovoliunlem2  21646  ovolicc2lem3  21662  ovolicc2lem4  21663  nulmbl2  21679  volsup  21698  ioombl1lem4  21703  dyadmax  21739  vitalilem2  21750  vitalilem5  21753  mbfi1flimlem  21861  itg2seq  21881  itg2addlem  21897  itgcn  21981  limciun  22030  rolle  22123  c1lip3  22132  dvfsumrlim  22164  itgsubst  22182  aannenlem1  22455  aalioulem2  22460  aalioulem3  22461  aalioulem5  22463  aalioulem6  22464  aaliou  22465  ulmcaulem  22520  ulmcau  22521  ulmss  22523  ulmbdd  22524  ulmcn  22525  ulmdvlem3  22528  mtest  22530  iblulm  22533  itgulm  22534  rlimcnp  23020  xrlimcnp  23023  rlimcxp  23028  o1cxp  23029  amgm  23045  ftalem2  23072  isppw2  23114  mumullem2  23179  2sqlem6  23369  chtppilimlem2  23384  chtppilim  23385  pntrsumbnd2  23477  pntlem3  23519  isperp2  23797  axeuclidlem  23938  axeuclid  23939  cusgrares  24145  edgwlk  24204  usgrnloop  24238  redwlk  24281  cusconngra  24349  wlkiswwlk1  24363  wlkiswwlk2lem4  24367  usg2wlkeq  24381  wwlknred  24396  wwlkm1edg  24408  clwlkisclwwlklem2a  24458  clwlkisclwwlklem1  24460  usgravd00  24592  cusgraisrusgra  24611  rusgraprop2  24615  rusgraprop3  24616  frisusgranb  24670  2pthfrgrarn  24682  2pthfrgrarn2  24683  2pthfrgra  24684  3cyclfrgra  24688  frgrancvvdeq  24716  frgrancvvdgeq  24717  nmoub3i  25361  ubthlem1  25459  ubthlem3  25461  ocsh  25874  chintcli  25922  chscllem2  26229  nmopub2tALT  26501  nmfnleub2  26518  lnconi  26625  riesz1  26657  rnbra  26699  leopadd  26724  leopmuli  26725  leoptr  26729  dmdbr3  26897  dmdbr4  26898  dmdbr5  26900  mdsl0  26902  mdsymlem6  27000  cdj1i  27025  xrge0infss  27245  lmxrge0  27567  lgambdd  28216  cvmlift2lem12  28396  nofulllem4  29039  finixpnum  29612  heicant  29624  itg2addnclem  29641  itg2addnclem3  29643  itg2addnc  29644  opnrebl2  29714  neibastop1  29778  neibastop2lem  29779  neibastop3  29781  filbcmb  29832  nninfnub  29845  geomcau  29853  sstotbnd2  29871  isbndx  29879  equivbnd  29887  prdsbnd  29890  heibor1lem  29906  heiborlem1  29908  heibor  29918  rrncmslem  29929  ghomco  29946  intidl  30027  elrfirn2  30230  isnacs3  30244  rencldnfilem  30356  kelac1  30613  acsfn1p  30753  neglimc  31189  stoweidlem7  31307  fourierdlem73  31480  ply1mulgsumlem1  32059  ply1mulgsumlem3  32061  ply1mulgsumlem4  32062  snlindsntor  32145  pclclN  34687  lauteq  34891  ltrnid  34931  mapdh9a  36587