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

Theorem ralrimdv 2880
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)
Hypothesis
Ref Expression
ralrimdv.1  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
Assertion
Ref Expression
ralrimdv  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Distinct variable groups:    ph, x    ps, x
Allowed substitution hints:    ch( x)    A( x)

Proof of Theorem ralrimdv
StepHypRef Expression
1 ralrimdv.1 . . . 4  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
21imp 429 . . 3  |-  ( (
ph  /\  ps )  ->  ( x  e.  A  ->  ch ) )
32ralrimiv 2876 . 2  |-  ( (
ph  /\  ps )  ->  A. x  e.  A  ch )
43ex 434 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  ralrimdva  2882  ralrimdvaOLD  2883  ralrimivv  2884  wefrc  4873  oneqmin  6618  nneneq  7697  cflm  8626  coflim  8637  isf32lem12  8740  axdc3lem2  8827  zorn2lem7  8878  axpre-sup  9542  infmrcl  10518  zmax  11175  zbtwnre  11176  supxrunb2  11508  fzrevral  11758  islss4  17391  topbas  19240  elcls3  19350  neips  19380  clslp  19415  subbascn  19521  cnpnei  19531  fgss2  20110  fbflim2  20213  alexsubALTlem3  20284  alexsubALTlem4  20285  alexsubALT  20286  metcnp3  20778  aalioulem3  22464  brbtwn2  23884  hial0  25695  hial02  25696  ococss  25887  lnopmi  26595  adjlnop  26681  pjss2coi  26759  pj3cor1i  26804  strlem3a  26847  hstrlem3a  26855  mdbr3  26892  mdbr4  26893  dmdmd  26895  dmdbr3  26900  dmdbr4  26901  dmdbr5  26903  ssmd2  26907  mdslmd1i  26924  mdsymlem7  27004  cdj1i  27028  cdj3lem2b  27032  ghomf1olem  28509  comppfsc  29779  lindslinindsimp2  32137  trintALT  32761  lub0N  33986  glb0N  33990  hlrelat2  34199  snatpsubN  34546  pmaple  34557  pclclN  34687  pclfinN  34696  pclfinclN  34746  ltrneq2  34944  trlval2  34959  trlord  35365
  Copyright terms: Public domain W3C validator