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

Theorem ralrimdva 2796
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
Hypothesis
Ref Expression
ralrimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralrimdva  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Distinct variable groups:    ph, x    ps, x
Allowed substitution hints:    ch( x)    A( x)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 424 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32com23 74 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2795 1  |-  ( ph  ->  ( 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:  ralxfrd  4737  isoselem  6061  resixpfo  7100  findcard  7347  ordtypelem2  7488  alephinit  7976  isfin2-2  8199  axpre-sup  9044  nnsub  10038  ublbneg  10560  xralrple  10791  supxrunb1  10898  expnlbnd2  11510  faclbnd4lem4  11587  hashbc  11702  cau3lem  12158  limsupbnd2  12277  climrlim2  12341  climshftlem  12368  subcn2  12388  isercoll  12461  climsup  12463  serf0  12474  iseralt  12478  incexclem  12616  sqr2irr  12848  pclem  13212  prmpwdvds  13272  vdwlem10  13358  vdwlem13  13361  ramtlecl  13368  ramub  13381  ramcl  13397  iscatd  13898  clatleglb  14553  grpinveu  14839  issubg4  14961  gexdvds  15218  sylow2alem2  15252  obselocv  16955  tgcn  17316  tgcnp  17317  lmconst  17325  cncls2  17337  cncls  17338  cnntr  17339  lmss  17362  cnt0  17410  isnrm2  17422  isreg2  17441  cmpsublem  17462  cmpsub  17463  tgcmp  17464  islly2  17547  kgencn2  17589  txdis  17664  txlm  17680  kqt0lem  17768  isr0  17769  regr1lem2  17772  cmphaushmeo  17832  cfinufil  17960  ufilen  17962  flimopn  18007  fbflim2  18009  fclsnei  18051  fclsbas  18053  fclsrest  18056  flimfnfcls  18060  fclscmp  18062  ufilcmp  18064  isfcf  18066  fcfnei  18067  cnpfcf  18073  tsmsres  18173  tsmsxp  18184  blbas  18460  prdsbl  18521  metss  18538  metcnp3  18570  bndth  18983  lebnumii  18991  iscfil3  19226  iscmet3lem1  19244  equivcfil  19252  equivcau  19253  ellimc3  19766  lhop1  19898  dvfsumrlim  19915  ftc1lem6  19925  fta1g  20090  dgrco  20193  plydivex  20214  fta1  20225  vieta1  20229  ulmshftlem  20305  ulmcaulem  20310  mtest  20320  cxpcn3lem  20631  cxploglim  20816  ftalem3  20857  dchrisumlem3  21185  pntibnd  21287  ostth2lem2  21328  grpoinveu  21810  isgrp2d  21823  nmcvcn  22191  blocnilem  22305  ubthlem3  22374  htthlem  22420  spansni  23059  bra11  23611  lmxrge0  24337  ftc1cnnc  26279  fnemeet2  26396  fnejoin2  26398  incsequz2  26453  geomcau  26465  caushft  26467  sstotbnd2  26483  isbnd2  26492  totbndbnd  26498  ismtybndlem  26515  heibor  26530  climinf  27708  ralbinrald  27953  ralxfrd2  28072  glb0N  29991  atlatle  30118  cvlcvr1  30137  ltrnid  30932  ltrneq2  30945
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