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

Theorem ralimdva 2784
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 2783 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2705
This theorem is referenced by:  ralimdv  2785  wereu2  4579  onint  4775  f1mpt  6007  isores3  6055  caofrss  6337  caoftrn  6339  sorpssuni  6531  sorpssint  6532  smogt  6629  tfrlem1  6636  fisupg  7355  ixpfi2  7405  fissuni  7411  indexfi  7414  wemaplem2  7516  rankonidlem  7754  ac5num  7917  acni2  7927  acndom2  7935  alephle  7969  dfac5  8009  cfsmolem  8150  isf34lem7  8259  isf34lem6  8260  fin1a2s  8294  acncc  8320  ttukeylem6  8394  fpwwe2lem8  8512  gchina  8574  inar1  8650  tskord  8655  grudomon  8692  grur1a  8694  fimaxre  9955  uzwo  10539  uzwoOLD  10540  xrsupsslem  10885  xrinfmsslem  10886  rexanre  12150  rexuz3  12152  rexico  12157  cau3lem  12158  limsupval2  12274  rlim2lt  12291  rlim3  12292  lo1bdd2  12318  lo1bddrp  12319  o1lo1  12331  climrlim2  12341  2clim  12366  o1co  12380  rlimcn1  12382  rlimcn2  12384  climcn1  12385  climcn2  12386  subcn2  12388  o1of2  12406  rlimo1  12410  o1rlimmul  12412  lo1add  12420  lo1mul  12421  climsqz  12434  climsqz2  12435  rlimsqzlem  12442  lo1le  12445  climbdd  12465  caucvgrlem  12466  caucvgrlem2  12468  caurcvg2  12471  iseralt  12478  cvgcmp  12595  cvgcmpce  12597  gcdcllem1  13011  pcfac  13268  pockthg  13274  infpnlem1  13278  prmreclem2  13285  prmreclem3  13286  vdwlem11  13359  vdwlem13  13361  vdwnnlem3  13365  isacs2  13878  acsfn1  13886  acsfn2  13888  catpropd  13935  drsdirfi  14395  ipodrsima  14591  isacs5  14598  mrelatglb  14610  mrelatlub  14612  isgrpinv  14855  issubg4  14961  gexdvds  15218  gexcl3  15221  sylow2blem3  15256  cyggeninv  15493  dprdff  15570  issubdrg  15893  islmhm2  16114  cygznlem3  16850  neiptopnei  17196  cncnp  17344  isnrm2  17422  isreg2  17441  2ndcdisj  17519  islly2  17547  dislly  17560  kgen2ss  17587  ptbasfi  17613  ptclsg  17647  prdstopn  17660  txtube  17672  txlm  17680  isr0  17769  filuni  17917  alexsubALTlem3  18080  ptcmplem3  18085  ptcmplem4  18086  tgpt0  18148  tsmsxplem1  18182  prdsmet  18400  metequiv2  18540  metcnpi3  18576  isngp4  18658  nmoleub  18765  addcnlem  18894  rescncf  18927  cncfco  18937  evth  18984  lebnumlem3  18988  xlebnum  18990  nmoleub2lem2  19124  nmhmcn  19128  lmmcvg  19214  cmetcaulem  19241  caubl  19260  bcth3  19284  ovollb2lem  19384  ovoliunlem2  19399  ovolicc2lem3  19415  ovolicc2lem4  19416  nulmbl2  19431  volsup  19450  ioombl1lem4  19455  dyadmax  19490  vitalilem2  19501  vitalilem5  19504  mbfi1flimlem  19614  itg2seq  19634  itg2addlem  19650  itgcn  19734  limciun  19781  rolle  19874  c1lip3  19883  dvfsumrlim  19915  itgsubst  19933  aannenlem1  20245  aalioulem2  20250  aalioulem3  20251  aalioulem5  20253  aalioulem6  20254  aaliou  20255  ulmcaulem  20310  ulmcau  20311  ulmss  20313  ulmbdd  20314  ulmcn  20315  ulmdvlem3  20318  mtest  20320  iblulm  20323  itgulm  20324  rlimcnp  20804  xrlimcnp  20807  rlimcxp  20812  o1cxp  20813  amgm  20829  ftalem2  20856  isppw2  20898  mumullem2  20963  2sqlem6  21153  chtppilimlem2  21168  chtppilim  21169  pntrsumbnd2  21261  pntlem3  21303  cusgrares  21481  usgrnloop  21563  redwlk  21606  cusconngra  21663  nmoub3i  22274  ubthlem1  22372  ubthlem3  22374  ocsh  22785  chintcli  22833  chscllem2  23140  nmopub2tALT  23412  nmfnleub2  23429  lnconi  23536  riesz1  23568  rnbra  23610  leopadd  23635  leopmuli  23636  leoptr  23640  dmdbr3  23808  dmdbr4  23809  dmdbr5  23811  mdsl0  23813  mdsymlem6  23911  cdj1i  23936  lmxrge0  24337  lgambdd  24821  cvmlift2lem12  25001  dedekind  25187  dedekindle  25188  nofulllem4  25660  axeuclidlem  25901  axeuclid  25902  itg2addnclem  26256  itg2addnclem3  26258  itg2addnc  26259  opnrebl2  26324  neibastop1  26388  neibastop2lem  26389  neibastop3  26391  filbcmb  26442  nninfnub  26455  geomcau  26465  sstotbnd2  26483  isbndx  26491  equivbnd  26499  prdsbnd  26502  heibor1lem  26518  heiborlem1  26520  heibor  26530  rrncmslem  26541  ghomco  26558  intidl  26639  elrfirn2  26750  isnacs3  26764  rencldnfilem  26881  kelac1  27138  acsfn1p  27484  stoweidlem7  27732  usg2wlkeq  28304  cusgraisrusgra  28377  frisusgranb  28387  2pthfrgrarn  28399  2pthfrgrarn2  28400  2pthfrgra  28401  3cyclfrgra  28405  frgrancvvdeq  28431  frgrancvvdgeq  28432  pclclN  30688  lauteq  30892  ltrnid  30932  mapdh9a  32588
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2710
  Copyright terms: Public domain W3C validator