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

Theorem ralimdva 2655
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 1610 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2654 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 1701   A.wral 2577
This theorem is referenced by:  ralimdv  2656  wereu2  4427  onint  4623  f1mpt  5827  isores3  5874  caofrss  6152  caoftrn  6154  sorpssuni  6328  sorpssint  6329  smogt  6426  tfrlem1  6433  fisupg  7150  ixpfi2  7199  fissuni  7205  indexfi  7208  wemaplem2  7307  rankonidlem  7545  ac5num  7708  acni2  7718  acndom2  7726  alephle  7760  dfac5  7800  cfsmolem  7941  isf34lem7  8050  isf34lem6  8051  fin1a2s  8085  acncc  8111  ttukeylem6  8186  fpwwe2lem8  8304  gchina  8366  inar1  8442  tskord  8447  grudomon  8484  grur1a  8486  fimaxre  9746  uzwo  10328  uzwoOLD  10329  xrsupsslem  10672  xrinfmsslem  10673  rexanre  11877  rexuz3  11879  rexico  11884  cau3lem  11885  limsupval2  12001  rlim2lt  12018  rlim3  12019  lo1bdd2  12045  lo1bddrp  12046  o1lo1  12058  climrlim2  12068  2clim  12093  o1co  12107  rlimcn1  12109  rlimcn2  12111  climcn1  12112  climcn2  12113  subcn2  12115  o1of2  12133  rlimo1  12137  o1rlimmul  12139  lo1add  12147  lo1mul  12148  climsqz  12161  climsqz2  12162  rlimsqzlem  12169  lo1le  12172  caucvgrlem  12192  caucvgrlem2  12194  caurcvg2  12197  iseralt  12204  cvgcmp  12321  cvgcmpce  12323  gcdcllem1  12737  pcfac  12994  pockthg  13000  infpnlem1  13004  prmreclem2  13011  prmreclem3  13012  vdwlem11  13085  vdwlem13  13087  vdwnnlem3  13091  isacs2  13604  acsfn1  13612  acsfn2  13614  catpropd  13661  drsdirfi  14121  ipodrsima  14317  isacs5  14324  mrelatglb  14336  mrelatlub  14338  isgrpinv  14581  issubg4  14687  gexdvds  14944  gexcl3  14947  sylow2blem3  14982  cyggeninv  15219  dprdff  15296  issubdrg  15619  islmhm2  15844  cygznlem3  16579  cncnp  17065  isnrm2  17142  isreg2  17161  2ndcdisj  17238  islly2  17266  dislly  17279  kgen2ss  17306  ptbasfi  17332  ptclsg  17365  prdstopn  17378  txtube  17390  txlm  17398  isr0  17484  filuni  17632  alexsubALTlem3  17795  ptcmplem3  17800  ptcmplem4  17801  tgpt0  17853  tsmsxplem1  17887  prdsmet  17986  metequiv2  18108  metcnpi3  18144  isngp4  18185  nmoleub  18292  addcnlem  18420  rescncf  18453  cncfco  18463  evth  18510  lebnumlem3  18514  xlebnum  18516  nmoleub2lem2  18650  nmhmcn  18654  lmmcvg  18740  cmetcaulem  18767  caubl  18786  bcth3  18806  ovollb2lem  18900  ovoliunlem2  18915  ovolicc2lem3  18931  ovolicc2lem4  18932  nulmbl2  18947  volsup  18966  ioombl1lem4  18971  dyadmax  19006  vitalilem2  19017  vitalilem5  19020  mbfi1flimlem  19130  itg2seq  19150  itg2addlem  19166  itgcn  19250  limciun  19297  rolle  19390  c1lip3  19399  dvfsumrlim  19431  itgsubst  19449  aannenlem1  19761  aalioulem2  19766  aalioulem3  19767  aalioulem5  19769  aalioulem6  19770  aaliou  19771  ulmcaulem  19824  ulmcau  19825  ulmss  19827  ulmbdd  19828  ulmcn  19829  ulmdvlem3  19832  mtest  19834  iblulm  19836  itgulm  19837  rlimcnp  20313  xrlimcnp  20316  rlimcxp  20321  o1cxp  20322  amgm  20338  ftalem2  20364  isppw2  20406  mumullem2  20471  2sqlem6  20661  chtppilimlem2  20676  chtppilim  20677  pntrsumbnd2  20769  pntlem3  20811  nmoub3i  21406  ubthlem1  21504  ubthlem3  21506  ocsh  21917  chintcli  21965  chscllem2  22272  nmopub2tALT  22544  nmfnleub2  22561  lnconi  22668  riesz1  22700  rnbra  22742  leopadd  22767  leopmuli  22768  leoptr  22772  dmdbr3  22940  dmdbr4  22941  dmdbr5  22943  mdsl0  22945  mdsymlem6  23043  cdj1i  23068  lmxrge0  23406  cvmlift2lem12  24129  dedekind  24368  dedekindle  24369  nofulllem4  24744  axeuclidlem  24976  axeuclid  24977  itg2addnclem  25317  itg2addnc  25319  opnrebl2  25385  neibastop1  25457  neibastop2lem  25458  neibastop3  25460  filbcmb  25581  nninfnub  25610  geomcau  25624  sstotbnd2  25646  isbndx  25654  equivbnd  25662  prdsbnd  25665  heibor1lem  25681  heiborlem1  25683  heibor  25693  rrncmslem  25704  ghomco  25721  intidl  25802  elrfirn2  25919  isnacs3  25933  rencldnfilem  26051  kelac1  26309  acsfn1p  26655  stoweidlem7  26904  usgrnloop  27467  redwlk  27502  cusconngra  27560  frisusgranb  27589  2pthfrgrarn  27601  2pthfrgrarn2  27602  2pthfrgra  27603  3cyclfrgra  27607  frgrancvvdeq  27634  frgrancvvdgeq  27635  pclclN  29898  lauteq  30102  ltrnid  30142  mapdh9a  31798
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-nf 1536  df-ral 2582
  Copyright terms: Public domain W3C validator