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

Theorem ralrimdva 2811
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 2810 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2725
This theorem is referenced by:  ralxfrd  4511  isoselem  6037  resixpfo  7306  findcard  7556  ordtypelem2  7738  alephinit  8270  isfin2-2  8493  axpre-sup  9341  nnsub  10365  ublbneg  10944  xralrple  11180  supxrunb1  11287  expnlbnd2  12000  faclbnd4lem4  12077  hashbc  12211  cau3lem  12847  limsupbnd2  12966  climrlim2  13030  climshftlem  13057  subcn2  13077  isercoll  13150  climsup  13152  serf0  13163  iseralt  13167  incexclem  13304  sqr2irr  13536  pclem  13910  prmpwdvds  13970  vdwlem10  14056  vdwlem13  14059  ramtlecl  14066  ramub  14079  ramcl  14095  iscatd  14616  clatleglb  15301  mrcmndind  15499  grpinveu  15577  issubg4  15705  gexdvds  16088  sylow2alem2  16122  obselocv  18158  tgcn  18861  tgcnp  18862  lmconst  18870  cncls2  18882  cncls  18883  cnntr  18884  lmss  18907  cnt0  18955  isnrm2  18967  isreg2  18986  cmpsublem  19007  cmpsub  19008  tgcmp  19009  islly2  19093  kgencn2  19135  txdis  19210  txlm  19226  kqt0lem  19314  isr0  19315  regr1lem2  19318  cmphaushmeo  19378  cfinufil  19506  ufilen  19508  flimopn  19553  fbflim2  19555  fclsnei  19597  fclsbas  19599  fclsrest  19602  flimfnfcls  19606  fclscmp  19608  ufilcmp  19610  isfcf  19612  fcfnei  19613  cnpfcf  19619  tsmsresOLD  19722  tsmsres  19723  tsmsxp  19734  blbas  20010  prdsbl  20071  metss  20088  metcnp3  20120  bndth  20535  lebnumii  20543  iscfil3  20789  iscmet3lem1  20807  equivcfil  20815  equivcau  20816  ellimc3  21359  lhop1  21491  dvfsumrlim  21508  ftc1lem6  21518  fta1g  21644  dgrco  21747  plydivex  21768  fta1  21779  vieta1  21783  ulmshftlem  21859  ulmcaulem  21864  mtest  21874  cxpcn3lem  22190  cxploglim  22376  ftalem3  22417  dchrisumlem3  22745  pntibnd  22847  ostth2lem2  22888  grpoinveu  23714  isgrp2d  23727  nmcvcn  24095  blocnilem  24209  ubthlem3  24278  htthlem  24324  spansni  24965  bra11  25517  lmxrge0  26387  fin2so  28421  ftc1cnnc  28471  fnemeet2  28593  fnejoin2  28595  incsequz2  28650  geomcau  28660  caushft  28662  sstotbnd2  28678  isbnd2  28687  totbndbnd  28693  ismtybndlem  28710  heibor  28725  climinf  29784  ralbinrald  30028  ralxfrd2  30142  atlatle  32970  cvlcvr1  32989  ltrnid  33784  ltrneq2  33797
  Copyright terms: Public domain W3C validator