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

Theorem ralimdva 2623
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 1607 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2622 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 1686   A.wral 2545
This theorem is referenced by:  ralimdv  2624  wereu2  4392  onint  4588  f1mpt  5787  isores3  5834  caofrss  6112  caoftrn  6114  sorpssuni  6288  sorpssint  6289  smogt  6386  tfrlem1  6393  fisupg  7107  ixpfi2  7156  fissuni  7162  indexfi  7165  wemaplem2  7264  rankonidlem  7502  ac5num  7665  acni2  7675  acndom2  7683  alephle  7717  dfac5  7757  cfsmolem  7898  isf34lem7  8007  isf34lem6  8008  fin1a2s  8042  acncc  8068  ttukeylem6  8143  fpwwe2lem8  8261  gchina  8323  inar1  8399  tskord  8404  grudomon  8441  grur1a  8443  fimaxre  9703  uzwo  10283  uzwoOLD  10284  xrsupsslem  10627  xrinfmsslem  10628  rexanre  11832  rexuz3  11834  rexico  11839  cau3lem  11840  limsupval2  11956  rlim2lt  11973  rlim3  11974  lo1bdd2  12000  lo1bddrp  12001  o1lo1  12013  climrlim2  12023  2clim  12048  o1co  12062  rlimcn1  12064  rlimcn2  12066  climcn1  12067  climcn2  12068  subcn2  12070  o1of2  12088  rlimo1  12092  o1rlimmul  12094  lo1add  12102  lo1mul  12103  climsqz  12116  climsqz2  12117  rlimsqzlem  12124  lo1le  12127  caucvgrlem  12147  caucvgrlem2  12149  caurcvg2  12152  iseralt  12159  cvgcmp  12276  cvgcmpce  12278  gcdcllem1  12692  pcfac  12949  pockthg  12955  infpnlem1  12959  prmreclem2  12966  prmreclem3  12967  vdwlem11  13040  vdwlem13  13042  vdwnnlem3  13046  isacs2  13557  acsfn1  13565  acsfn2  13567  catpropd  13614  drsdirfi  14074  ipodrsima  14270  isacs5  14277  mrelatglb  14289  mrelatlub  14291  isgrpinv  14534  issubg4  14640  gexdvds  14897  gexcl3  14900  sylow2blem3  14935  cyggeninv  15172  dprdff  15249  issubdrg  15572  islmhm2  15797  cygznlem3  16525  cncnp  17011  isnrm2  17088  isreg2  17107  2ndcdisj  17184  islly2  17212  dislly  17225  kgen2ss  17252  ptbasfi  17278  ptclsg  17311  prdstopn  17324  txtube  17336  txlm  17344  isr0  17430  filuni  17582  alexsubALTlem3  17745  ptcmplem3  17750  ptcmplem4  17751  tgpt0  17803  tsmsxplem1  17837  prdsmet  17936  metequiv2  18058  metcnpi3  18094  isngp4  18135  nmoleub  18242  addcnlem  18370  rescncf  18403  cncfco  18413  evth  18459  lebnumlem3  18463  xlebnum  18465  nmoleub2lem2  18599  nmhmcn  18603  lmmcvg  18689  cmetcaulem  18716  caubl  18735  bcth3  18755  ovollb2lem  18849  ovoliunlem2  18864  ovolicc2lem3  18880  ovolicc2lem4  18881  nulmbl2  18896  volsup  18915  ioombl1lem4  18920  dyadmax  18955  vitalilem2  18966  vitalilem5  18969  mbfi1flimlem  19079  itg2seq  19099  itg2addlem  19115  itgcn  19199  limciun  19246  rolle  19339  c1lip3  19348  dvfsumrlim  19380  itgsubst  19398  aannenlem1  19710  aalioulem2  19715  aalioulem3  19716  aalioulem5  19718  aalioulem6  19719  aaliou  19720  ulmcaulem  19773  ulmcau  19774  ulmss  19776  ulmbdd  19777  ulmcn  19778  ulmdvlem3  19781  mtest  19783  iblulm  19785  itgulm  19786  rlimcnp  20262  xrlimcnp  20265  rlimcxp  20270  o1cxp  20271  amgm  20287  ftalem2  20313  isppw2  20355  mumullem2  20420  2sqlem6  20610  chtppilimlem2  20625  chtppilim  20626  pntrsumbnd2  20718  pntlem3  20760  nmoub3i  21353  ubthlem1  21451  ubthlem3  21453  ocsh  21864  chintcli  21912  chscllem2  22219  nmopub2tALT  22491  nmfnleub2  22508  lnconi  22615  riesz1  22647  rnbra  22689  leopadd  22714  leopmuli  22715  leoptr  22719  dmdbr3  22887  dmdbr4  22888  dmdbr5  22890  mdsl0  22892  mdsymlem6  22990  cdj1i  23015  lmxrge0  23377  cvmlift2lem12  23847  dedekind  24084  dedekindle  24085  nofulllem4  24361  axeuclidlem  24592  axeuclid  24593  itg2addnclem  24933  itg2addnc  24935  mgmlion  25348  intfmu2  25530  islimrs3  25592  islimrs4  25593  icmpmon  25827  bhp3  26188  opnrebl2  26247  neibastop1  26319  neibastop2lem  26320  neibastop3  26322  filbcmb  26443  nninfnub  26472  geomcau  26486  sstotbnd2  26509  isbndx  26517  equivbnd  26525  prdsbnd  26528  heibor1lem  26544  heiborlem1  26546  heibor  26556  rrncmslem  26567  ghomco  26584  intidl  26665  elrfirn2  26782  isnacs3  26796  rencldnfilem  26914  kelac1  27172  acsfn1p  27518  stoweidlem7  27767  pclclN  30153  lauteq  30357  ltrnid  30397  mapdh9a  32053
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator