MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralimdva Unicode version

Theorem ralimdva 2583
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
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2582 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   A.wral 2509
This theorem is referenced by:  ralimdv  2584  wereu2  4283  onint  4477  f1mpt  5637  isores3  5684  caofrss  5962  caoftrn  5964  sorpssuni  6138  sorpssint  6139  smogt  6270  tfrlem1  6277  fisupg  6990  ixpfi2  7038  fissuni  7044  indexfi  7047  wemaplem2  7146  rankonidlem  7384  ac5num  7547  acni2  7557  acndom2  7565  alephle  7599  dfac5  7639  cfsmolem  7780  isf34lem7  7889  isf34lem6  7890  fin1a2s  7924  acncc  7950  ttukeylem6  8025  fpwwe2lem8  8139  gchina  8201  inar1  8277  tskord  8282  grudomon  8319  grur1a  8321  fimaxre  9581  uzwo  10160  uzwoOLD  10161  xrsupsslem  10503  xrinfmsslem  10504  rexanre  11707  rexuz3  11709  rexico  11714  cau3lem  11715  limsupval2  11831  rlim2lt  11848  rlim3  11849  lo1bdd2  11875  lo1bddrp  11876  o1lo1  11888  climrlim2  11898  2clim  11923  o1co  11937  rlimcn1  11939  rlimcn2  11941  climcn1  11942  climcn2  11943  subcn2  11945  o1of2  11963  rlimo1  11967  o1rlimmul  11969  lo1add  11977  lo1mul  11978  climsqz  11991  climsqz2  11992  rlimsqzlem  11999  lo1le  12002  caucvgrlem  12022  caucvgrlem2  12024  caurcvg2  12027  iseralt  12034  cvgcmp  12151  cvgcmpce  12153  gcdcllem1  12564  pcfac  12821  pockthg  12827  infpnlem1  12831  prmreclem2  12838  prmreclem3  12839  vdwlem11  12912  vdwlem13  12914  vdwnnlem3  12918  isacs2  13400  acsfn1  13407  acsfn2  13409  catpropd  13456  drsdirfi  13916  ipodrsima  14112  isacs5  14119  mrelatglb  14122  mrelatlub  14124  isgrpinv  14367  issubg4  14473  gexdvds  14730  gexcl3  14733  sylow2blem3  14768  cyggeninv  15005  dprdff  15082  issubdrg  15405  islmhm2  15630  cygznlem3  16355  cncnp  16841  isnrm2  16918  isreg2  16937  2ndcdisj  17014  islly2  17042  dislly  17055  kgen2ss  17082  ptbasfi  17108  ptclsg  17141  prdstopn  17154  txtube  17166  txlm  17174  isr0  17260  filuni  17412  alexsubALTlem3  17575  ptcmplem3  17580  ptcmplem4  17581  tgpt0  17633  tsmsxplem1  17667  prdsmet  17766  metequiv2  17888  metcnpi3  17924  isngp4  17965  nmoleub  18072  addcnlem  18200  rescncf  18233  cncfco  18243  evth  18289  lebnumlem3  18293  xlebnum  18295  nmoleub2lem2  18429  nmhmcn  18433  lmmcvg  18519  cmetcaulem  18546  caubl  18565  bcth3  18585  ovollb2lem  18679  ovoliunlem2  18694  ovolicc2lem3  18710  ovolicc2lem4  18711  nulmbl2  18726  volsup  18745  ioombl1lem4  18750  dyadmax  18785  vitalilem2  18796  vitalilem5  18799  mbfi1flimlem  18909  itg2seq  18929  itg2addlem  18945  itgcn  19029  limciun  19076  rolle  19169  c1lip3  19178  dvfsumrlim  19210  itgsubst  19228  aannenlem1  19540  aalioulem2  19545  aalioulem3  19546  aalioulem5  19548  aalioulem6  19549  aaliou  19550  ulmcaulem  19603  ulmcau  19604  ulmss  19606  ulmbdd  19607  ulmcn  19608  ulmdvlem3  19611  mtest  19613  iblulm  19615  itgulm  19616  rlimcnp  20092  xrlimcnp  20095  rlimcxp  20100  o1cxp  20101  amgm  20117  ftalem2  20143  isppw2  20185  mumullem2  20250  2sqlem6  20440  chtppilimlem2  20455  chtppilim  20456  pntrsumbnd2  20548  pntlem3  20590  nmoub3i  21181  ubthlem1  21279  ubthlem3  21281  ocsh  21692  chintcli  21740  chscllem2  22065  nmopub2tALT  22319  nmfnleub2  22336  lnconi  22443  riesz1  22475  rnbra  22517  leopadd  22542  leopmuli  22543  leoptr  22547  dmdbr3  22715  dmdbr4  22716  dmdbr5  22718  mdsl0  22720  mdsymlem6  22818  cdj1i  22843  cvmlift2lem12  23016  dedekind  23252  dedekindle  23253  axfelem8  23521  axeuclidlem  23764  axeuclid  23765  mgmlion  24503  intfmu2  24685  islimrs3  24747  islimrs4  24748  icmpmon  24982  bhp3  25343  opnrebl2  25402  neibastop1  25474  neibastop2lem  25475  neibastop3  25477  filbcmb  25598  nninfnub  25627  geomcau  25641  sstotbnd2  25664  isbndx  25672  equivbnd  25680  prdsbnd  25683  heibor1lem  25699  heiborlem1  25701  heibor  25711  rrncmslem  25722  ghomco  25739  intidl  25820  elrfirn2  25937  isnacs3  25951  rencldnfilem  26069  kelac1  26327  acsfn1p  26673  pclclN  28839  lauteq  29043  ltrnid  29083  mapdh9a  30739
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 2513
  Copyright terms: Public domain W3C validator