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

Theorem ralrimdva 2875
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.)
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 ) )
21expimpd 603 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  ->  ch ) )
32expcomd 438 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2873 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1819   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
This theorem is referenced by:  ralxfrd  4670  isoselem  6238  resixpfo  7526  findcard  7777  ordtypelem2  7962  alephinit  8493  isfin2-2  8716  axpre-sup  9563  nnsub  10595  ublbneg  11191  xralrple  11429  supxrunb1  11536  expnlbnd2  12300  faclbnd4lem4  12377  hashbc  12506  cau3lem  13199  limsupbnd2  13318  climrlim2  13382  climshftlem  13409  subcn2  13429  isercoll  13502  climsup  13504  serf0  13515  iseralt  13519  incexclem  13660  sqrt2irr  13994  pclem  14374  prmpwdvds  14434  vdwlem10  14520  vdwlem13  14523  ramtlecl  14530  ramub  14543  ramcl  14559  iscatd  15090  clatleglb  15883  mrcmndind  16124  grpinveu  16211  issubg4  16347  gexdvds  16731  sylow2alem2  16765  obselocv  18886  scmatscm  19142  tgcn  19880  tgcnp  19881  lmconst  19889  cncls2  19901  cncls  19902  cnntr  19903  lmss  19926  cnt0  19974  isnrm2  19986  isreg2  20005  cmpsublem  20026  cmpsub  20027  tgcmp  20028  islly2  20111  kgencn2  20184  txdis  20259  txlm  20275  kqt0lem  20363  isr0  20364  regr1lem2  20367  cmphaushmeo  20427  cfinufil  20555  ufilen  20557  flimopn  20602  fbflim2  20604  fclsnei  20646  fclsbas  20648  fclsrest  20651  flimfnfcls  20655  fclscmp  20657  ufilcmp  20659  isfcf  20661  fcfnei  20662  cnpfcf  20668  tsmsresOLD  20771  tsmsres  20772  tsmsxp  20783  blbas  21059  prdsbl  21120  metss  21137  metcnp3  21169  bndth  21584  lebnumii  21592  iscfil3  21838  iscmet3lem1  21856  equivcfil  21864  equivcau  21865  ellimc3  22409  lhop1  22541  dvfsumrlim  22558  ftc1lem6  22568  fta1g  22694  dgrco  22798  plydivex  22819  fta1  22830  vieta1  22834  ulmshftlem  22910  ulmcaulem  22915  mtest  22925  cxpcn3lem  23247  cxploglim  23433  ftalem3  23474  dchrisumlem3  23802  pntibnd  23904  ostth2lem2  23945  grpoinveu  25351  isgrp2d  25364  nmcvcn  25732  blocnilem  25846  ubthlem3  25915  htthlem  25961  spansni  26602  bra11  27154  lmxrge0  28095  mrsubff1  29071  msubff1  29113  fin2so  30245  ftc1cnnc  30294  fnemeet2  30390  fnejoin2  30392  incsequz2  30447  geomcau  30457  caushft  30459  sstotbnd2  30475  isbnd2  30484  totbndbnd  30490  ismtybndlem  30507  heibor  30522  climinf  31815  ralbinrald  32407  ralxfrd2  32567  snlindsntorlem  33215  atlatle  35188  cvlcvr1  35207  ltrnid  36002  ltrneq2  36015
  Copyright terms: Public domain W3C validator