Theorem ralimdva 2832

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		ax-5 1671	. 2 |- ( ph -> A. x ph )
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	hbralimdaa 2825	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671

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

This theorem is referenced by:  ralimdv  2834  ralimdvva  2906  wereu2  4826  f1mpt  6084  isores3  6136  caofrss  6464  caoftrn  6466  sorpssuni  6480  sorpssint  6481  onint  6517  smogt  6939  fisupg  7672  ixpfi2  7721  fissuni  7728  indexfi  7731  wemaplem2  7873  rankonidlem  8147  ac5num  8318  acni2  8328  acndom2  8336  alephle  8370  dfac5  8410  cfsmolem  8551  isf34lem7  8660  isf34lem6  8661  fin1a2s  8695  acncc  8721  ttukeylem6  8795  fpwwe2lem8  8916  gchina  8978  inar1  9054  tskord  9059  grudomon  9096  grur1a  9098  dedekind  9645  dedekindle  9646  fimaxre  10389  uzwo  11029  uzwoOLD  11030  xrsupsslem  11381  xrinfmsslem  11382  rexanre  12953  rexuz3  12955  rexico  12960  cau3lem  12961  limsupval2  13077  rlim2lt  13094  rlim3  13095  lo1bdd2  13121  lo1bddrp  13122  o1lo1  13134  climrlim2  13144  2clim  13169  o1co  13183  rlimcn1  13185  rlimcn2  13187  climcn1  13188  climcn2  13189  subcn2  13191  o1of2  13209  rlimo1  13213  o1rlimmul  13215  lo1add  13223  lo1mul  13224  climsqz  13237  climsqz2  13238  rlimsqzlem  13245  lo1le  13248  climbdd  13268  caucvgrlem  13269  caucvgrlem2  13271  caurcvg2  13274  iseralt  13281  cvgcmp  13398  cvgcmpce  13400  gcdcllem1  13814  pcfac  14080  pockthg  14086  infpnlem1  14090  prmreclem2  14097  prmreclem3  14098  vdwlem11  14171  vdwlem13  14173  vdwnnlem3  14177  isacs2  14711  acsfn1  14719  acsfn2  14721  catpropd  14768  drsdirfi  15228  ipodrsima  15455  isacs5  15462  mrelatglb  15474  mrelatlub  15476  isgrpinv  15708  issubg4  15820  gsmsymgreqlem2  16056  gexdvds  16205  gexcl3  16208  sylow2blem3  16243  cyggeninv  16482  dprdff  16619  dprdffOLD  16625  issubdrg  17014  islmhm2  17243  cygznlem3  18128  mdetdiagid  18539  mdetunilem9  18559  neiptopnei  18869  cncnp  19017  isnrm2  19095  isreg2  19114  2ndcdisj  19193  islly2  19221  dislly  19234  kgen2ss  19261  ptbasfi  19287  ptclsg  19321  prdstopn  19334  txtube  19346  txlm  19354  isr0  19443  filuni  19591  alexsubALTlem3  19754  ptcmplem3  19759  ptcmplem4  19760  tgpt0  19822  tsmsxplem1  19860  prdsmet  20078  metequiv2  20218  metcnpi3  20254  isngp4  20336  nmoleub  20443  addcnlem  20573  rescncf  20606  cncfco  20616  evth  20664  lebnumlem3  20668  xlebnum  20670  nmoleub2lem2  20804  nmhmcn  20808  lmmcvg  20905  cmetcaulem  20932  caubl  20951  bcth3  20975  ovollb2lem  21104  ovoliunlem2  21119  ovolicc2lem3  21135  ovolicc2lem4  21136  nulmbl2  21152  volsup  21171  ioombl1lem4  21176  dyadmax  21212  vitalilem2  21223  vitalilem5  21226  mbfi1flimlem  21334  itg2seq  21354  itg2addlem  21370  itgcn  21454  limciun  21503  rolle  21596  c1lip3  21605  dvfsumrlim  21637  itgsubst  21655  aannenlem1  21928  aalioulem2  21933  aalioulem3  21934  aalioulem5  21936  aalioulem6  21937  aaliou  21938  ulmcaulem  21993  ulmcau  21994  ulmss  21996  ulmbdd  21997  ulmcn  21998  ulmdvlem3  22001  mtest  22003  iblulm  22006  itgulm  22007  rlimcnp  22493  xrlimcnp  22496  rlimcxp  22501  o1cxp  22502  amgm  22518  ftalem2  22545  isppw2  22587  mumullem2  22652  2sqlem6  22842  chtppilimlem2  22857  chtppilim  22858  pntrsumbnd2  22950  pntlem3  22992  isperp2  23252  axeuclidlem  23361  axeuclid  23362  cusgrares  23533  usgrnloop  23615  redwlk  23658  cusconngra  23715  nmoub3i  24326  ubthlem1  24424  ubthlem3  24426  ocsh  24839  chintcli  24887  chscllem2  25194  nmopub2tALT  25466  nmfnleub2  25483  lnconi  25590  riesz1  25622  rnbra  25664  leopadd  25689  leopmuli  25690  leoptr  25694  dmdbr3  25862  dmdbr4  25863  dmdbr5  25865  mdsl0  25867  mdsymlem6  25965  cdj1i  25990  xrge0infss  26205  lmxrge0  26528  lgambdd  27168  cvmlift2lem12  27348  nofulllem4  27991  finixpnum  28563  heicant  28575  itg2addnclem  28592  itg2addnclem3  28594  itg2addnc  28595  opnrebl2  28665  neibastop1  28729  neibastop2lem  28730  neibastop3  28732  filbcmb  28783  nninfnub  28796  geomcau  28804  sstotbnd2  28822  isbndx  28830  equivbnd  28838  prdsbnd  28841  heibor1lem  28857  heiborlem1  28859  heibor  28869  rrncmslem  28880  ghomco  28897  intidl  28978  elrfirn2  29181  isnacs3  29195  rencldnfilem  29308  kelac1  29565  acsfn1p  29705  stoweidlem7  29951  usg2wlkeq  30438  edgwlk  30443  wlkiswwlk1  30473  wlkiswwlk2lem4  30477  wwlknred  30504  wwlkm1edg  30516  clwlkisclwwlklem2a  30596  clwlkisclwwlklem1  30598  usgravd00  30687  cusgraisrusgra  30700  rusgraprop2  30703  rusgraprop3  30704  frisusgranb  30738  2pthfrgrarn  30750  2pthfrgrarn2  30751  2pthfrgra  30752  3cyclfrgra  30756  frgrancvvdeq  30784  frgrancvvdgeq  30785  fsuppmapnn0fiub0  30950  gsummptnn0fz  30959  mptcoe1fsupp  30987  gsummoncoe1  30997  ply1mulgsumlem1  30999  ply1mulgsumlem3  31001  ply1mulgsumlem4  31002  cply1coe0bi  31005  scmatscmid  31024  scmatdmat  31063  scmatsubcl  31064  scmatmulcl  31066  snlindsntor  31138  cpmatmcllem  31208  m2pminv2lem  31239  decpmatmulsumfsupp  31261  pmatcollpw1lem1  31262  pmatcollpw2lem  31265  pmatcollpwfi  31270  pm2mpf1  31287  mptcoe1matfsupp  31290  mp2pm2mplem4  31297  pm2mpmhmlem1  31306  pm2mp  31312  cpdmat  31328  cpscmat  31329  cpmidpmatlem3  31359  cayhamlem4  31376  pclclN  33874  lauteq  34078  ltrnid  34118  mapdh9a  35774