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 434 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32com23 78 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2795 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  ralxfrd  4494  isoselem  6019  resixpfo  7289  findcard  7539  ordtypelem2  7721  alephinit  8253  isfin2-2  8476  axpre-sup  9323  nnsub  10347  ublbneg  10926  xralrple  11162  supxrunb1  11269  expnlbnd2  11978  faclbnd4lem4  12055  hashbc  12189  cau3lem  12825  limsupbnd2  12944  climrlim2  13008  climshftlem  13035  subcn2  13055  isercoll  13128  climsup  13130  serf0  13141  iseralt  13145  incexclem  13281  sqr2irr  13513  pclem  13887  prmpwdvds  13947  vdwlem10  14033  vdwlem13  14036  ramtlecl  14043  ramub  14056  ramcl  14072  iscatd  14593  clatleglb  15278  mrcmndind  15475  grpinveu  15551  issubg4  15679  gexdvds  16062  sylow2alem2  16096  obselocv  17994  tgcn  18697  tgcnp  18698  lmconst  18706  cncls2  18718  cncls  18719  cnntr  18720  lmss  18743  cnt0  18791  isnrm2  18803  isreg2  18822  cmpsublem  18843  cmpsub  18844  tgcmp  18845  islly2  18929  kgencn2  18971  txdis  19046  txlm  19062  kqt0lem  19150  isr0  19151  regr1lem2  19154  cmphaushmeo  19214  cfinufil  19342  ufilen  19344  flimopn  19389  fbflim2  19391  fclsnei  19433  fclsbas  19435  fclsrest  19438  flimfnfcls  19442  fclscmp  19444  ufilcmp  19446  isfcf  19448  fcfnei  19449  cnpfcf  19455  tsmsresOLD  19558  tsmsres  19559  tsmsxp  19570  blbas  19846  prdsbl  19907  metss  19924  metcnp3  19956  bndth  20371  lebnumii  20379  iscfil3  20625  iscmet3lem1  20643  equivcfil  20651  equivcau  20652  ellimc3  21195  lhop1  21327  dvfsumrlim  21344  ftc1lem6  21354  fta1g  21523  dgrco  21626  plydivex  21647  fta1  21658  vieta1  21662  ulmshftlem  21738  ulmcaulem  21743  mtest  21753  cxpcn3lem  22069  cxploglim  22255  ftalem3  22296  dchrisumlem3  22624  pntibnd  22726  ostth2lem2  22767  grpoinveu  23531  isgrp2d  23544  nmcvcn  23912  blocnilem  24026  ubthlem3  24095  htthlem  24141  spansni  24782  bra11  25334  lmxrge0  26235  fin2so  28257  ftc1cnnc  28307  fnemeet2  28429  fnejoin2  28431  incsequz2  28486  geomcau  28496  caushft  28498  sstotbnd2  28514  isbnd2  28523  totbndbnd  28529  ismtybndlem  28546  heibor  28561  climinf  29622  ralbinrald  29866  ralxfrd2  29980  atlatle  32535  cvlcvr1  32554  ltrnid  33349  ltrneq2  33362
  Copyright terms: Public domain W3C validator