Theorem ralimdva 2596

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

Syntax hints:   -> wi 6   /\ wa 360   e. wcel 1621   A.wral 2518

This theorem is referenced by:  ralimdv  2597  wereu2  4362  onint  4558  f1mpt  5719  isores3  5766  caofrss  6044  caoftrn  6046  sorpssuni  6220  sorpssint  6221  smogt  6352  tfrlem1  6359  fisupg  7073  ixpfi2  7122  fissuni  7128  indexfi  7131  wemaplem2  7230  rankonidlem  7468  ac5num  7631  acni2  7641  acndom2  7649  alephle  7683  dfac5  7723  cfsmolem  7864  isf34lem7  7973  isf34lem6  7974  fin1a2s  8008  acncc  8034  ttukeylem6  8109  fpwwe2lem8  8227  gchina  8289  inar1  8365  tskord  8370  grudomon  8407  grur1a  8409  fimaxre  9669  uzwo  10249  uzwoOLD  10250  xrsupsslem  10592  xrinfmsslem  10593  rexanre  11796  rexuz3  11798  rexico  11803  cau3lem  11804  limsupval2  11920  rlim2lt  11937  rlim3  11938  lo1bdd2  11964  lo1bddrp  11965  o1lo1  11977  climrlim2  11987  2clim  12012  o1co  12026  rlimcn1  12028  rlimcn2  12030  climcn1  12031  climcn2  12032  subcn2  12034  o1of2  12052  rlimo1  12056  o1rlimmul  12058  lo1add  12066  lo1mul  12067  climsqz  12080  climsqz2  12081  rlimsqzlem  12088  lo1le  12091  caucvgrlem  12111  caucvgrlem2  12113  caurcvg2  12116  iseralt  12123  cvgcmp  12240  cvgcmpce  12242  gcdcllem1  12653  pcfac  12910  pockthg  12916  infpnlem1  12920  prmreclem2  12927  prmreclem3  12928  vdwlem11  13001  vdwlem13  13003  vdwnnlem3  13007  isacs2  13518  acsfn1  13526  acsfn2  13528  catpropd  13575  drsdirfi  14035  ipodrsima  14231  isacs5  14238  mrelatglb  14250  mrelatlub  14252  isgrpinv  14495  issubg4  14601  gexdvds  14858  gexcl3  14861  sylow2blem3  14896  cyggeninv  15133  dprdff  15210  issubdrg  15533  islmhm2  15758  cygznlem3  16486  cncnp  16972  isnrm2  17049  isreg2  17068  2ndcdisj  17145  islly2  17173  dislly  17186  kgen2ss  17213  ptbasfi  17239  ptclsg  17272  prdstopn  17285  txtube  17297  txlm  17305  isr0  17391  filuni  17543  alexsubALTlem3  17706  ptcmplem3  17711  ptcmplem4  17712  tgpt0  17764  tsmsxplem1  17798  prdsmet  17897  metequiv2  18019  metcnpi3  18055  isngp4  18096  nmoleub  18203  addcnlem  18331  rescncf  18364  cncfco  18374  evth  18420  lebnumlem3  18424  xlebnum  18426  nmoleub2lem2  18560  nmhmcn  18564  lmmcvg  18650  cmetcaulem  18677  caubl  18696  bcth3  18716  ovollb2lem  18810  ovoliunlem2  18825  ovolicc2lem3  18841  ovolicc2lem4  18842  nulmbl2  18857  volsup  18876  ioombl1lem4  18881  dyadmax  18916  vitalilem2  18927  vitalilem5  18930  mbfi1flimlem  19040  itg2seq  19060  itg2addlem  19076  itgcn  19160  limciun  19207  rolle  19300  c1lip3  19309  dvfsumrlim  19341  itgsubst  19359  aannenlem1  19671  aalioulem2  19676  aalioulem3  19677  aalioulem5  19679  aalioulem6  19680  aaliou  19681  ulmcaulem  19734  ulmcau  19735  ulmss  19737  ulmbdd  19738  ulmcn  19739  ulmdvlem3  19742  mtest  19744  iblulm  19746  itgulm  19747  rlimcnp  20223  xrlimcnp  20226  rlimcxp  20231  o1cxp  20232  amgm  20248  ftalem2  20274  isppw2  20316  mumullem2  20381  2sqlem6  20571  chtppilimlem2  20586  chtppilim  20587  pntrsumbnd2  20679  pntlem3  20721  nmoub3i  21312  ubthlem1  21410  ubthlem3  21412  ocsh  21823  chintcli  21871  chscllem2  22178  nmopub2tALT  22450  nmfnleub2  22467  lnconi  22574  riesz1  22606  rnbra  22648  leopadd  22673  leopmuli  22674  leoptr  22678  dmdbr3  22846  dmdbr4  22847  dmdbr5  22849  mdsl0  22851  mdsymlem6  22949  cdj1i  22974  cvmlift2lem12  23218  dedekind  23454  dedekindle  23455  axfelem8  23723  axeuclidlem  23966  axeuclid  23967  mgmlion  24705  intfmu2  24887  islimrs3  24949  islimrs4  24950  icmpmon  25184  bhp3  25545  opnrebl2  25604  neibastop1  25676  neibastop2lem  25677  neibastop3  25679  filbcmb  25800  nninfnub  25829  geomcau  25843  sstotbnd2  25866  isbndx  25874  equivbnd  25882  prdsbnd  25885  heibor1lem  25901  heiborlem1  25903  heibor  25913  rrncmslem  25924  ghomco  25941  intidl  26022  elrfirn2  26139  isnacs3  26153  rencldnfilem  26271  kelac1  26529  acsfn1p  26875  stoweidlem7  27125  pclclN  29330  lauteq  29534  ltrnid  29574  mapdh9a  31230

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692

This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2523