Theorem ralimdva 2744

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

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   A.wral 2666

This theorem is referenced by:  ralimdv  2745  wereu2  4539  onint  4734  f1mpt  5966  isores3  6014  caofrss  6296  caoftrn  6298  sorpssuni  6490  sorpssint  6491  smogt  6588  tfrlem1  6595  fisupg  7314  ixpfi2  7363  fissuni  7369  indexfi  7372  wemaplem2  7472  rankonidlem  7710  ac5num  7873  acni2  7883  acndom2  7891  alephle  7925  dfac5  7965  cfsmolem  8106  isf34lem7  8215  isf34lem6  8216  fin1a2s  8250  acncc  8276  ttukeylem6  8350  fpwwe2lem8  8468  gchina  8530  inar1  8606  tskord  8611  grudomon  8648  grur1a  8650  fimaxre  9911  uzwo  10495  uzwoOLD  10496  xrsupsslem  10841  xrinfmsslem  10842  rexanre  12105  rexuz3  12107  rexico  12112  cau3lem  12113  limsupval2  12229  rlim2lt  12246  rlim3  12247  lo1bdd2  12273  lo1bddrp  12274  o1lo1  12286  climrlim2  12296  2clim  12321  o1co  12335  rlimcn1  12337  rlimcn2  12339  climcn1  12340  climcn2  12341  subcn2  12343  o1of2  12361  rlimo1  12365  o1rlimmul  12367  lo1add  12375  lo1mul  12376  climsqz  12389  climsqz2  12390  rlimsqzlem  12397  lo1le  12400  climbdd  12420  caucvgrlem  12421  caucvgrlem2  12423  caurcvg2  12426  iseralt  12433  cvgcmp  12550  cvgcmpce  12552  gcdcllem1  12966  pcfac  13223  pockthg  13229  infpnlem1  13233  prmreclem2  13240  prmreclem3  13241  vdwlem11  13314  vdwlem13  13316  vdwnnlem3  13320  isacs2  13833  acsfn1  13841  acsfn2  13843  catpropd  13890  drsdirfi  14350  ipodrsima  14546  isacs5  14553  mrelatglb  14565  mrelatlub  14567  isgrpinv  14810  issubg4  14916  gexdvds  15173  gexcl3  15176  sylow2blem3  15211  cyggeninv  15448  dprdff  15525  issubdrg  15848  islmhm2  16069  cygznlem3  16805  neiptopnei  17151  cncnp  17298  isnrm2  17376  isreg2  17395  2ndcdisj  17472  islly2  17500  dislly  17513  kgen2ss  17540  ptbasfi  17566  ptclsg  17600  prdstopn  17613  txtube  17625  txlm  17633  isr0  17722  filuni  17870  alexsubALTlem3  18033  ptcmplem3  18038  ptcmplem4  18039  tgpt0  18101  tsmsxplem1  18135  prdsmet  18353  metequiv2  18493  metcnpi3  18529  isngp4  18611  nmoleub  18718  addcnlem  18847  rescncf  18880  cncfco  18890  evth  18937  lebnumlem3  18941  xlebnum  18943  nmoleub2lem2  19077  nmhmcn  19081  lmmcvg  19167  cmetcaulem  19194  caubl  19213  bcth3  19237  ovollb2lem  19337  ovoliunlem2  19352  ovolicc2lem3  19368  ovolicc2lem4  19369  nulmbl2  19384  volsup  19403  ioombl1lem4  19408  dyadmax  19443  vitalilem2  19454  vitalilem5  19457  mbfi1flimlem  19567  itg2seq  19587  itg2addlem  19603  itgcn  19687  limciun  19734  rolle  19827  c1lip3  19836  dvfsumrlim  19868  itgsubst  19886  aannenlem1  20198  aalioulem2  20203  aalioulem3  20204  aalioulem5  20206  aalioulem6  20207  aaliou  20208  ulmcaulem  20263  ulmcau  20264  ulmss  20266  ulmbdd  20267  ulmcn  20268  ulmdvlem3  20271  mtest  20273  iblulm  20276  itgulm  20277  rlimcnp  20757  xrlimcnp  20760  rlimcxp  20765  o1cxp  20766  amgm  20782  ftalem2  20809  isppw2  20851  mumullem2  20916  2sqlem6  21106  chtppilimlem2  21121  chtppilim  21122  pntrsumbnd2  21214  pntlem3  21256  cusgrares  21434  usgrnloop  21516  redwlk  21559  cusconngra  21616  nmoub3i  22227  ubthlem1  22325  ubthlem3  22327  ocsh  22738  chintcli  22786  chscllem2  23093  nmopub2tALT  23365  nmfnleub2  23382  lnconi  23489  riesz1  23521  rnbra  23563  leopadd  23588  leopmuli  23589  leoptr  23593  dmdbr3  23761  dmdbr4  23762  dmdbr5  23764  mdsl0  23766  mdsymlem6  23864  cdj1i  23889  lmxrge0  24290  lgambdd  24774  cvmlift2lem12  24954  dedekind  25140  dedekindle  25141  nofulllem4  25573  axeuclidlem  25805  axeuclid  25806  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  opnrebl2  26214  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  filbcmb  26332  nninfnub  26345  geomcau  26355  sstotbnd2  26373  isbndx  26381  equivbnd  26389  prdsbnd  26392  heibor1lem  26408  heiborlem1  26410  heibor  26420  rrncmslem  26431  ghomco  26448  intidl  26529  elrfirn2  26640  isnacs3  26654  rencldnfilem  26771  kelac1  27029  acsfn1p  27375  stoweidlem7  27623  frisusgranb  28101  2pthfrgrarn  28113  2pthfrgrarn2  28114  2pthfrgra  28115  3cyclfrgra  28119  frgrancvvdeq  28145  frgrancvvdgeq  28146  pclclN  30373  lauteq  30577  ltrnid  30617  mapdh9a  32273

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671