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

Theorem ralrimdv 2841
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 430 . . 3  |-  ( (
ph  /\  ps )  ->  ( x  e.  A  ->  ch ) )
32ralrimiv 2837 . 2  |-  ( (
ph  /\  ps )  ->  A. x  e.  A  ch )
43ex 435 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1868   A.wral 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2780
This theorem is referenced by:  ralrimdva  2843  ralrimdvaOLD  2844  ralrimivv  2845  wefrc  4844  oneqmin  6643  nneneq  7758  cflm  8681  coflim  8692  isf32lem12  8795  axdc3lem2  8882  zorn2lem7  8933  axpre-sup  9594  infmrclOLD  10594  zmax  11262  zbtwnre  11263  supxrunb2  11607  fzrevral  11880  islss4  18173  topbas  19975  elcls3  20086  neips  20116  clslp  20151  subbascn  20257  cnpnei  20267  comppfsc  20534  fgss2  20876  fbflim2  20979  alexsubALTlem3  21051  alexsubALTlem4  21052  alexsubALT  21053  metcnp3  21542  aalioulem3  23277  brbtwn2  24922  hial0  26741  hial02  26742  ococss  26932  lnopmi  27639  adjlnop  27725  pjss2coi  27803  pj3cor1i  27848  strlem3a  27891  hstrlem3a  27899  mdbr3  27936  mdbr4  27937  dmdmd  27939  dmdbr3  27944  dmdbr4  27945  dmdbr5  27947  ssmd2  27951  mdslmd1i  27968  mdsymlem7  28048  cdj1i  28072  cdj3lem2b  28076  ghomf1olem  30308  lub0N  32674  glb0N  32678  hlrelat2  32887  snatpsubN  33234  pmaple  33245  pclclN  33375  pclfinN  33384  pclfinclN  33434  ltrneq2  33632  trlval2  33648  trlord  34055  trintALT  37139  lindslinindsimp2  39530
  Copyright terms: Public domain W3C validator