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

Theorem ralimdva 2706
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 1624 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2705 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 1715   A.wral 2628
This theorem is referenced by:  ralimdv  2707  wereu2  4493  onint  4689  f1mpt  5907  isores3  5955  caofrss  6237  caoftrn  6239  sorpssuni  6428  sorpssint  6429  smogt  6526  tfrlem1  6533  fisupg  7252  ixpfi2  7301  fissuni  7307  indexfi  7310  wemaplem2  7409  rankonidlem  7647  ac5num  7810  acni2  7820  acndom2  7828  alephle  7862  dfac5  7902  cfsmolem  8043  isf34lem7  8152  isf34lem6  8153  fin1a2s  8187  acncc  8213  ttukeylem6  8288  fpwwe2lem8  8406  gchina  8468  inar1  8544  tskord  8549  grudomon  8586  grur1a  8588  fimaxre  9848  uzwo  10432  uzwoOLD  10433  xrsupsslem  10778  xrinfmsslem  10779  rexanre  12037  rexuz3  12039  rexico  12044  cau3lem  12045  limsupval2  12161  rlim2lt  12178  rlim3  12179  lo1bdd2  12205  lo1bddrp  12206  o1lo1  12218  climrlim2  12228  2clim  12253  o1co  12267  rlimcn1  12269  rlimcn2  12271  climcn1  12272  climcn2  12273  subcn2  12275  o1of2  12293  rlimo1  12297  o1rlimmul  12299  lo1add  12307  lo1mul  12308  climsqz  12321  climsqz2  12322  rlimsqzlem  12329  lo1le  12332  climbdd  12352  caucvgrlem  12353  caucvgrlem2  12355  caurcvg2  12358  iseralt  12365  cvgcmp  12482  cvgcmpce  12484  gcdcllem1  12898  pcfac  13155  pockthg  13161  infpnlem1  13165  prmreclem2  13172  prmreclem3  13173  vdwlem11  13246  vdwlem13  13248  vdwnnlem3  13252  isacs2  13765  acsfn1  13773  acsfn2  13775  catpropd  13822  drsdirfi  14282  ipodrsima  14478  isacs5  14485  mrelatglb  14497  mrelatlub  14499  isgrpinv  14742  issubg4  14848  gexdvds  15105  gexcl3  15108  sylow2blem3  15143  cyggeninv  15380  dprdff  15457  issubdrg  15780  islmhm2  16005  cygznlem3  16740  cncnp  17226  isnrm2  17303  isreg2  17322  2ndcdisj  17399  islly2  17427  dislly  17440  kgen2ss  17467  ptbasfi  17493  ptclsg  17526  prdstopn  17539  txtube  17551  txlm  17559  isr0  17645  filuni  17793  alexsubALTlem3  17956  ptcmplem3  17961  ptcmplem4  17962  tgpt0  18014  tsmsxplem1  18048  prdsmet  18147  metequiv2  18269  metcnpi3  18305  isngp4  18346  nmoleub  18453  addcnlem  18582  rescncf  18615  cncfco  18625  evth  18672  lebnumlem3  18676  xlebnum  18678  nmoleub2lem2  18812  nmhmcn  18816  lmmcvg  18902  cmetcaulem  18929  caubl  18948  bcth3  18968  ovollb2lem  19062  ovoliunlem2  19077  ovolicc2lem3  19093  ovolicc2lem4  19094  nulmbl2  19109  volsup  19128  ioombl1lem4  19133  dyadmax  19168  vitalilem2  19179  vitalilem5  19182  mbfi1flimlem  19292  itg2seq  19312  itg2addlem  19328  itgcn  19412  limciun  19459  rolle  19552  c1lip3  19561  dvfsumrlim  19593  itgsubst  19611  aannenlem1  19923  aalioulem2  19928  aalioulem3  19929  aalioulem5  19931  aalioulem6  19932  aaliou  19933  ulmcaulem  19988  ulmcau  19989  ulmss  19991  ulmbdd  19992  ulmcn  19993  ulmdvlem3  19996  mtest  19998  iblulm  20001  itgulm  20002  rlimcnp  20482  xrlimcnp  20485  rlimcxp  20490  o1cxp  20491  amgm  20507  ftalem2  20534  isppw2  20576  mumullem2  20641  2sqlem6  20831  chtppilimlem2  20846  chtppilim  20847  pntrsumbnd2  20939  pntlem3  20981  nmoub3i  21664  ubthlem1  21762  ubthlem3  21764  ocsh  22175  chintcli  22223  chscllem2  22530  nmopub2tALT  22802  nmfnleub2  22819  lnconi  22926  riesz1  22958  rnbra  23000  leopadd  23025  leopmuli  23026  leoptr  23030  dmdbr3  23198  dmdbr4  23199  dmdbr5  23201  mdsl0  23203  mdsymlem6  23301  cdj1i  23326  neiptopnei  23644  lmxrge0  23692  lgambdd  24269  cvmlift2lem12  24448  dedekind  24671  dedekindle  24672  nofulllem4  25100  axeuclidlem  25332  axeuclid  25333  itg2addnclem  25675  itg2addnc  25677  opnrebl2  25743  neibastop1  25815  neibastop2lem  25816  neibastop3  25818  filbcmb  25939  nninfnub  25968  geomcau  25982  sstotbnd2  26004  isbndx  26012  equivbnd  26020  prdsbnd  26023  heibor1lem  26039  heiborlem1  26041  heibor  26051  rrncmslem  26062  ghomco  26079  intidl  26160  elrfirn2  26277  isnacs3  26291  rencldnfilem  26409  kelac1  26667  acsfn1p  27013  stoweidlem7  27262  cusgrares  27637  usgrnloop  27709  redwlk  27744  cusconngra  27802  frisusgranb  27832  2pthfrgrarn  27844  2pthfrgrarn2  27845  2pthfrgra  27846  3cyclfrgra  27850  frgrancvvdeq  27877  frgrancvvdgeq  27878  pclclN  30151  lauteq  30355  ltrnid  30395  mapdh9a  32051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550  df-ral 2633
  Copyright terms: Public domain W3C validator