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

Theorem ralrimdv 3178
 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 410 . . 3 ((𝜑𝜓) → (𝑥𝐴𝜒))
32ralrimiv 3173 . 2 ((𝜑𝜓) → ∀𝑥𝐴 𝜒)
43ex 416 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2114  ∀wral 3130 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3135 This theorem is referenced by:  ralrimdva  3179  ralrimivv  3180  wefrc  5526  oneqmin  7505  nneneq  8688  cflm  9661  coflim  9672  isf32lem12  9775  axdc3lem2  9862  zorn2lem7  9913  axpre-sup  10580  zmax  12333  zbtwnre  12334  supxrunb2  12701  fzrevral  12987  lcmfdvdsb  15976  islss4  19725  topbas  21575  elcls3  21686  neips  21716  clslp  21751  subbascn  21857  cnpnei  21867  comppfsc  22135  fgss2  22477  fbflim2  22580  alexsubALTlem3  22652  alexsubALTlem4  22653  alexsubALT  22654  metcnp3  23145  aalioulem3  24928  brbtwn2  26697  hial0  28883  hial02  28884  ococss  29074  lnopmi  29781  adjlnop  29867  pjss2coi  29945  pj3cor1i  29990  strlem3a  30033  hstrlem3a  30041  mdbr3  30078  mdbr4  30079  dmdmd  30081  dmdbr3  30086  dmdbr4  30087  dmdbr5  30089  ssmd2  30093  mdslmd1i  30110  mdsymlem7  30190  cdj1i  30214  cdj3lem2b  30218  sat1el2xp  32700  fvineqsneu  34789  lub0N  36444  glb0N  36448  hlrelat2  36658  snatpsubN  37005  pmaple  37016  pclclN  37146  pclfinN  37155  pclfinclN  37205  ltrneq2  37403  trlval2  37418  trlord  37824  trintALT  41522  lindslinindsimp2  44812
 Copyright terms: Public domain W3C validator