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

Theorem ralrimdv 2819
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 427 . . 3  |-  ( (
ph  /\  ps )  ->  ( x  e.  A  ->  ch ) )
32ralrimiv 2815 . 2  |-  ( (
ph  /\  ps )  ->  A. x  e.  A  ch )
43ex 432 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   A.wral 2753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725
This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2758
This theorem is referenced by:  ralrimdva  2821  ralrimdvaOLD  2822  ralrimivv  2823  wefrc  4816  oneqmin  6622  nneneq  7737  cflm  8661  coflim  8672  isf32lem12  8775  axdc3lem2  8862  zorn2lem7  8913  axpre-sup  9575  infmrcl  10561  zmax  11223  zbtwnre  11224  supxrunb2  11564  fzrevral  11816  islss4  17926  topbas  19764  elcls3  19875  neips  19905  clslp  19940  subbascn  20046  cnpnei  20056  comppfsc  20323  fgss2  20665  fbflim2  20768  alexsubALTlem3  20839  alexsubALTlem4  20840  alexsubALT  20841  metcnp3  21333  aalioulem3  23020  brbtwn2  24612  hial0  26419  hial02  26420  ococss  26611  lnopmi  27318  adjlnop  27404  pjss2coi  27482  pj3cor1i  27527  strlem3a  27570  hstrlem3a  27578  mdbr3  27615  mdbr4  27616  dmdmd  27618  dmdbr3  27623  dmdbr4  27624  dmdbr5  27626  ssmd2  27630  mdslmd1i  27647  mdsymlem7  27727  cdj1i  27751  cdj3lem2b  27755  ghomf1olem  29873  lub0N  32187  glb0N  32191  hlrelat2  32400  snatpsubN  32747  pmaple  32758  pclclN  32888  pclfinN  32897  pclfinclN  32947  ltrneq2  33145  trlval2  33161  trlord  33568  trintALT  36692  lindslinindsimp2  38556
  Copyright terms: Public domain W3C validator