Theorem ralimdva 2789

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792

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

This theorem is referenced by:  ralimdv  2790  wereu2  4712  f1mpt  5969  isores3  6021  caofrss  6348  caoftrn  6350  sorpssuni  6364  sorpssint  6365  onint  6401  smogt  6820  fisupg  7552  ixpfi2  7601  fissuni  7608  indexfi  7611  wemaplem2  7753  rankonidlem  8027  ac5num  8198  acni2  8208  acndom2  8216  alephle  8250  dfac5  8290  cfsmolem  8431  isf34lem7  8540  isf34lem6  8541  fin1a2s  8575  acncc  8601  ttukeylem6  8675  fpwwe2lem8  8796  gchina  8858  inar1  8934  tskord  8939  grudomon  8976  grur1a  8978  dedekind  9525  dedekindle  9526  fimaxre  10269  uzwo  10909  uzwoOLD  10910  xrsupsslem  11261  xrinfmsslem  11262  rexanre  12826  rexuz3  12828  rexico  12833  cau3lem  12834  limsupval2  12950  rlim2lt  12967  rlim3  12968  lo1bdd2  12994  lo1bddrp  12995  o1lo1  13007  climrlim2  13017  2clim  13042  o1co  13056  rlimcn1  13058  rlimcn2  13060  climcn1  13061  climcn2  13062  subcn2  13064  o1of2  13082  rlimo1  13086  o1rlimmul  13088  lo1add  13096  lo1mul  13097  climsqz  13110  climsqz2  13111  rlimsqzlem  13118  lo1le  13121  climbdd  13141  caucvgrlem  13142  caucvgrlem2  13144  caurcvg2  13147  iseralt  13154  cvgcmp  13271  cvgcmpce  13273  gcdcllem1  13687  pcfac  13953  pockthg  13959  infpnlem1  13963  prmreclem2  13970  prmreclem3  13971  vdwlem11  14044  vdwlem13  14046  vdwnnlem3  14050  isacs2  14583  acsfn1  14591  acsfn2  14593  catpropd  14640  drsdirfi  15100  ipodrsima  15327  isacs5  15334  mrelatglb  15346  mrelatlub  15348  isgrpinv  15579  issubg4  15691  gsmsymgreqlem2  15927  gexdvds  16074  gexcl3  16077  sylow2blem3  16112  cyggeninv  16351  dprdff  16484  dprdffOLD  16490  issubdrg  16868  islmhm2  17096  cygznlem3  17977  mdetunilem9  18401  neiptopnei  18711  cncnp  18859  isnrm2  18937  isreg2  18956  2ndcdisj  19035  islly2  19063  dislly  19076  kgen2ss  19103  ptbasfi  19129  ptclsg  19163  prdstopn  19176  txtube  19188  txlm  19196  isr0  19285  filuni  19433  alexsubALTlem3  19596  ptcmplem3  19601  ptcmplem4  19602  tgpt0  19664  tsmsxplem1  19702  prdsmet  19920  metequiv2  20060  metcnpi3  20096  isngp4  20178  nmoleub  20285  addcnlem  20415  rescncf  20448  cncfco  20458  evth  20506  lebnumlem3  20510  xlebnum  20512  nmoleub2lem2  20646  nmhmcn  20650  lmmcvg  20747  cmetcaulem  20774  caubl  20793  bcth3  20817  ovollb2lem  20946  ovoliunlem2  20961  ovolicc2lem3  20977  ovolicc2lem4  20978  nulmbl2  20993  volsup  21012  ioombl1lem4  21017  dyadmax  21053  vitalilem2  21064  vitalilem5  21067  mbfi1flimlem  21175  itg2seq  21195  itg2addlem  21211  itgcn  21295  limciun  21344  rolle  21437  c1lip3  21446  dvfsumrlim  21478  itgsubst  21496  aannenlem1  21769  aalioulem2  21774  aalioulem3  21775  aalioulem5  21777  aalioulem6  21778  aaliou  21779  ulmcaulem  21834  ulmcau  21835  ulmss  21837  ulmbdd  21838  ulmcn  21839  ulmdvlem3  21842  mtest  21844  iblulm  21847  itgulm  21848  rlimcnp  22334  xrlimcnp  22337  rlimcxp  22342  o1cxp  22343  amgm  22359  ftalem2  22386  isppw2  22428  mumullem2  22493  2sqlem6  22683  chtppilimlem2  22698  chtppilim  22699  pntrsumbnd2  22791  pntlem3  22833  axeuclidlem  23159  axeuclid  23160  cusgrares  23331  usgrnloop  23413  redwlk  23456  cusconngra  23513  nmoub3i  24124  ubthlem1  24222  ubthlem3  24224  ocsh  24637  chintcli  24685  chscllem2  24992  nmopub2tALT  25264  nmfnleub2  25281  lnconi  25388  riesz1  25420  rnbra  25462  leopadd  25487  leopmuli  25488  leoptr  25492  dmdbr3  25660  dmdbr4  25661  dmdbr5  25663  mdsl0  25665  mdsymlem6  25763  cdj1i  25788  xrge0infss  26004  lmxrge0  26334  lgambdd  26975  cvmlift2lem12  27155  nofulllem4  27797  finixpnum  28367  heicant  28379  itg2addnclem  28396  itg2addnclem3  28398  itg2addnc  28399  opnrebl2  28469  neibastop1  28533  neibastop2lem  28534  neibastop3  28536  filbcmb  28587  nninfnub  28600  geomcau  28608  sstotbnd2  28626  isbndx  28634  equivbnd  28642  prdsbnd  28645  heibor1lem  28661  heiborlem1  28663  heibor  28673  rrncmslem  28684  ghomco  28701  intidl  28782  elrfirn2  28985  isnacs3  28999  rencldnfilem  29112  kelac1  29369  acsfn1p  29509  stoweidlem7  29755  usg2wlkeq  30242  edgwlk  30247  wlkiswwlk1  30277  wlkiswwlk2lem4  30281  wwlknred  30308  wwlkm1edg  30320  clwlkisclwwlklem2a  30400  clwlkisclwwlklem1  30402  usgravd00  30491  cusgraisrusgra  30504  rusgraprop2  30507  rusgraprop3  30508  frisusgranb  30542  2pthfrgrarn  30554  2pthfrgrarn2  30555  2pthfrgra  30556  3cyclfrgra  30560  frgrancvvdeq  30588  frgrancvvdgeq  30589  fsuppmapnn0fiub0  30750  scmatdmat  30806  scmatsubcl  30807  scmatmulcl  30809  pmatcollpw2lem  30820  mdetdiagid  30826  snlindsntor  30894  pclclN  33375  lauteq  33579  ltrnid  33619  mapdh9a  35275