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

Theorem ralrimdv 2951
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 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
Assertion
Ref Expression
ralrimdv (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥
Allowed substitution hints:   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimdv
StepHypRef Expression
1 ralrimdv.1 . . . 4 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
21imp 444 . . 3 ((𝜑𝜓) → (𝑥𝐴𝜒))
32ralrimiv 2948 . 2 ((𝜑𝜓) → ∀𝑥𝐴 𝜒)
43ex 449 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901
This theorem is referenced by:  ralrimdva  2952  ralrimivv  2953  wefrc  5032  oneqmin  6897  nneneq  8028  cflm  8955  coflim  8966  isf32lem12  9069  axdc3lem2  9156  zorn2lem7  9207  axpre-sup  9869  zmax  11661  zbtwnre  11662  supxrunb2  12022  fzrevral  12294  islss4  18783  topbas  20587  elcls3  20697  neips  20727  clslp  20762  subbascn  20868  cnpnei  20878  comppfsc  21145  fgss2  21488  fbflim2  21591  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  metcnp3  22155  aalioulem3  23893  brbtwn2  25585  hial0  27343  hial02  27344  ococss  27536  lnopmi  28243  adjlnop  28329  pjss2coi  28407  pj3cor1i  28452  strlem3a  28495  hstrlem3a  28503  mdbr3  28540  mdbr4  28541  dmdmd  28543  dmdbr3  28548  dmdbr4  28549  dmdbr5  28551  ssmd2  28555  mdslmd1i  28572  mdsymlem7  28652  cdj1i  28676  cdj3lem2b  28680  lub0N  33494  glb0N  33498  hlrelat2  33707  snatpsubN  34054  pmaple  34065  pclclN  34195  pclfinN  34204  pclfinclN  34254  ltrneq2  34452  trlval2  34468  trlord  34875  trintALT  38139  lindslinindsimp2  42046
  Copyright terms: Public domain W3C validator