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

Theorem ralimdva 2621
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 1605 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2620 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ralimdv  2622  wereu2  4390  onint  4586  f1mpt  5785  isores3  5832  caofrss  6110  caoftrn  6112  sorpssuni  6286  sorpssint  6287  smogt  6384  tfrlem1  6391  fisupg  7105  ixpfi2  7154  fissuni  7160  indexfi  7163  wemaplem2  7262  rankonidlem  7500  ac5num  7663  acni2  7673  acndom2  7681  alephle  7715  dfac5  7755  cfsmolem  7896  isf34lem7  8005  isf34lem6  8006  fin1a2s  8040  acncc  8066  ttukeylem6  8141  fpwwe2lem8  8259  gchina  8321  inar1  8397  tskord  8402  grudomon  8439  grur1a  8441  fimaxre  9701  uzwo  10281  uzwoOLD  10282  xrsupsslem  10625  xrinfmsslem  10626  rexanre  11830  rexuz3  11832  rexico  11837  cau3lem  11838  limsupval2  11954  rlim2lt  11971  rlim3  11972  lo1bdd2  11998  lo1bddrp  11999  o1lo1  12011  climrlim2  12021  2clim  12046  o1co  12060  rlimcn1  12062  rlimcn2  12064  climcn1  12065  climcn2  12066  subcn2  12068  o1of2  12086  rlimo1  12090  o1rlimmul  12092  lo1add  12100  lo1mul  12101  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  lo1le  12125  caucvgrlem  12145  caucvgrlem2  12147  caurcvg2  12150  iseralt  12157  cvgcmp  12274  cvgcmpce  12276  gcdcllem1  12690  pcfac  12947  pockthg  12953  infpnlem1  12957  prmreclem2  12964  prmreclem3  12965  vdwlem11  13038  vdwlem13  13040  vdwnnlem3  13044  isacs2  13555  acsfn1  13563  acsfn2  13565  catpropd  13612  drsdirfi  14072  ipodrsima  14268  isacs5  14275  mrelatglb  14287  mrelatlub  14289  isgrpinv  14532  issubg4  14638  gexdvds  14895  gexcl3  14898  sylow2blem3  14933  cyggeninv  15170  dprdff  15247  issubdrg  15570  islmhm2  15795  cygznlem3  16523  cncnp  17009  isnrm2  17086  isreg2  17105  2ndcdisj  17182  islly2  17210  dislly  17223  kgen2ss  17250  ptbasfi  17276  ptclsg  17309  prdstopn  17322  txtube  17334  txlm  17342  isr0  17428  filuni  17580  alexsubALTlem3  17743  ptcmplem3  17748  ptcmplem4  17749  tgpt0  17801  tsmsxplem1  17835  prdsmet  17934  metequiv2  18056  metcnpi3  18092  isngp4  18133  nmoleub  18240  addcnlem  18368  rescncf  18401  cncfco  18411  evth  18457  lebnumlem3  18461  xlebnum  18463  nmoleub2lem2  18597  nmhmcn  18601  lmmcvg  18687  cmetcaulem  18714  caubl  18733  bcth3  18753  ovollb2lem  18847  ovoliunlem2  18862  ovolicc2lem3  18878  ovolicc2lem4  18879  nulmbl2  18894  volsup  18913  ioombl1lem4  18918  dyadmax  18953  vitalilem2  18964  vitalilem5  18967  mbfi1flimlem  19077  itg2seq  19097  itg2addlem  19113  itgcn  19197  limciun  19244  rolle  19337  c1lip3  19346  dvfsumrlim  19378  itgsubst  19396  aannenlem1  19708  aalioulem2  19713  aalioulem3  19714  aalioulem5  19716  aalioulem6  19717  aaliou  19718  ulmcaulem  19771  ulmcau  19772  ulmss  19774  ulmbdd  19775  ulmcn  19776  ulmdvlem3  19779  mtest  19781  iblulm  19783  itgulm  19784  rlimcnp  20260  xrlimcnp  20263  rlimcxp  20268  o1cxp  20269  amgm  20285  ftalem2  20311  isppw2  20353  mumullem2  20418  2sqlem6  20608  chtppilimlem2  20623  chtppilim  20624  pntrsumbnd2  20716  pntlem3  20758  nmoub3i  21351  ubthlem1  21449  ubthlem3  21451  ocsh  21862  chintcli  21910  chscllem2  22217  nmopub2tALT  22489  nmfnleub2  22506  lnconi  22613  riesz1  22645  rnbra  22687  leopadd  22712  leopmuli  22713  leoptr  22717  dmdbr3  22885  dmdbr4  22886  dmdbr5  22888  mdsl0  22890  mdsymlem6  22988  cdj1i  23013  lmxrge0  23375  cvmlift2lem12  23845  dedekind  24082  dedekindle  24083  nofulllem4  24359  axeuclidlem  24590  axeuclid  24591  mgmlion  25337  intfmu2  25519  islimrs3  25581  islimrs4  25582  icmpmon  25816  bhp3  26177  opnrebl2  26236  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  filbcmb  26432  nninfnub  26461  geomcau  26475  sstotbnd2  26498  isbndx  26506  equivbnd  26514  prdsbnd  26517  heibor1lem  26533  heiborlem1  26535  heibor  26545  rrncmslem  26556  ghomco  26573  intidl  26654  elrfirn2  26771  isnacs3  26785  rencldnfilem  26903  kelac1  27161  acsfn1p  27507  stoweidlem7  27756  pclclN  30080  lauteq  30284  ltrnid  30324  mapdh9a  31980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator