Theorem ralimdva 2784

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

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		nfv 1672	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2783	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  ralimdv  2785  wereu2  4704  f1mpt  5961  isores3  6013  caofrss  6342  caoftrn  6344  sorpssuni  6358  sorpssint  6359  onint  6395  smogt  6814  fisupg  7548  ixpfi2  7597  fissuni  7604  indexfi  7607  wemaplem2  7749  rankonidlem  8023  ac5num  8194  acni2  8204  acndom2  8212  alephle  8246  dfac5  8286  cfsmolem  8427  isf34lem7  8536  isf34lem6  8537  fin1a2s  8571  acncc  8597  ttukeylem6  8671  fpwwe2lem8  8792  gchina  8854  inar1  8930  tskord  8935  grudomon  8972  grur1a  8974  dedekind  9521  dedekindle  9522  fimaxre  10265  uzwo  10905  uzwoOLD  10906  xrsupsslem  11257  xrinfmsslem  11258  rexanre  12818  rexuz3  12820  rexico  12825  cau3lem  12826  limsupval2  12942  rlim2lt  12959  rlim3  12960  lo1bdd2  12986  lo1bddrp  12987  o1lo1  12999  climrlim2  13009  2clim  13034  o1co  13048  rlimcn1  13050  rlimcn2  13052  climcn1  13053  climcn2  13054  subcn2  13056  o1of2  13074  rlimo1  13078  o1rlimmul  13080  lo1add  13088  lo1mul  13089  climsqz  13102  climsqz2  13103  rlimsqzlem  13110  lo1le  13113  climbdd  13133  caucvgrlem  13134  caucvgrlem2  13136  caurcvg2  13139  iseralt  13146  cvgcmp  13262  cvgcmpce  13264  gcdcllem1  13678  pcfac  13944  pockthg  13950  infpnlem1  13954  prmreclem2  13961  prmreclem3  13962  vdwlem11  14035  vdwlem13  14037  vdwnnlem3  14041  isacs2  14574  acsfn1  14582  acsfn2  14584  catpropd  14631  drsdirfi  15091  ipodrsima  15318  isacs5  15325  mrelatglb  15337  mrelatlub  15339  isgrpinv  15568  issubg4  15680  gsmsymgreqlem2  15916  gexdvds  16063  gexcl3  16066  sylow2blem3  16101  cyggeninv  16340  dprdff  16470  dprdffOLD  16476  issubdrg  16814  islmhm2  17041  cygznlem3  17844  mdetunilem9  18268  neiptopnei  18578  cncnp  18726  isnrm2  18804  isreg2  18823  2ndcdisj  18902  islly2  18930  dislly  18943  kgen2ss  18970  ptbasfi  18996  ptclsg  19030  prdstopn  19043  txtube  19055  txlm  19063  isr0  19152  filuni  19300  alexsubALTlem3  19463  ptcmplem3  19468  ptcmplem4  19469  tgpt0  19531  tsmsxplem1  19569  prdsmet  19787  metequiv2  19927  metcnpi3  19963  isngp4  20045  nmoleub  20152  addcnlem  20282  rescncf  20315  cncfco  20325  evth  20373  lebnumlem3  20377  xlebnum  20379  nmoleub2lem2  20513  nmhmcn  20517  lmmcvg  20614  cmetcaulem  20641  caubl  20660  bcth3  20684  ovollb2lem  20813  ovoliunlem2  20828  ovolicc2lem3  20844  ovolicc2lem4  20845  nulmbl2  20860  volsup  20879  ioombl1lem4  20884  dyadmax  20920  vitalilem2  20931  vitalilem5  20934  mbfi1flimlem  21042  itg2seq  21062  itg2addlem  21078  itgcn  21162  limciun  21211  rolle  21304  c1lip3  21313  dvfsumrlim  21345  itgsubst  21363  aannenlem1  21679  aalioulem2  21684  aalioulem3  21685  aalioulem5  21687  aalioulem6  21688  aaliou  21689  ulmcaulem  21744  ulmcau  21745  ulmss  21747  ulmbdd  21748  ulmcn  21749  ulmdvlem3  21752  mtest  21754  iblulm  21757  itgulm  21758  rlimcnp  22244  xrlimcnp  22247  rlimcxp  22252  o1cxp  22253  amgm  22269  ftalem2  22296  isppw2  22338  mumullem2  22403  2sqlem6  22593  chtppilimlem2  22608  chtppilim  22609  pntrsumbnd2  22701  pntlem3  22743  axeuclidlem  23031  axeuclid  23032  cusgrares  23203  usgrnloop  23285  redwlk  23328  cusconngra  23385  nmoub3i  23996  ubthlem1  24094  ubthlem3  24096  ocsh  24509  chintcli  24557  chscllem2  24864  nmopub2tALT  25136  nmfnleub2  25153  lnconi  25260  riesz1  25292  rnbra  25334  leopadd  25359  leopmuli  25360  leoptr  25364  dmdbr3  25532  dmdbr4  25533  dmdbr5  25535  mdsl0  25537  mdsymlem6  25635  cdj1i  25660  lmxrge0  26236  lgambdd  26871  cvmlift2lem12  27051  nofulllem4  27693  finixpnum  28258  heicant  28270  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  opnrebl2  28360  neibastop1  28424  neibastop2lem  28425  neibastop3  28427  filbcmb  28478  nninfnub  28491  geomcau  28499  sstotbnd2  28517  isbndx  28525  equivbnd  28533  prdsbnd  28536  heibor1lem  28552  heiborlem1  28554  heibor  28564  rrncmslem  28575  ghomco  28592  intidl  28673  elrfirn2  28877  isnacs3  28891  rencldnfilem  29004  kelac1  29261  acsfn1p  29401  stoweidlem7  29648  usg2wlkeq  30135  edgwlk  30140  wlkiswwlk1  30170  wlkiswwlk2lem4  30174  wwlknred  30201  wwlkm1edg  30213  clwlkisclwwlklem2a  30293  clwlkisclwwlklem1  30295  usgravd00  30384  cusgraisrusgra  30397  rusgraprop2  30400  rusgraprop3  30401  frisusgranb  30435  2pthfrgrarn  30447  2pthfrgrarn2  30448  2pthfrgra  30449  3cyclfrgra  30453  frgrancvvdeq  30481  frgrancvvdgeq  30482  snlindsntor  30714  pclclN  33108  lauteq  33312  ltrnid  33352  mapdh9a  35008