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

Theorem ralrimdv 3146
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 408 . . 3 ((𝜑𝜓) → (𝑥𝐴𝜒))
32ralrimiv 3139 . 2 ((𝜑𝜓) → ∀𝑥𝐴 𝜒)
43ex 414 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3062
This theorem is referenced by:  ralrimdva  3148  ralrimivv  3192  wefrc  5628  oneqmin  7736  nneneq  9156  nneneqOLD  9168  cflm  10191  coflim  10202  isf32lem12  10305  axdc3lem2  10392  zorn2lem7  10443  axpre-sup  11110  zmax  12875  zbtwnre  12876  supxrunb2  13245  fzrevral  13532  lcmfdvdsb  16524  islss4  20438  topbas  22338  elcls3  22450  neips  22480  clslp  22515  subbascn  22621  cnpnei  22631  comppfsc  22899  fgss2  23241  fbflim2  23344  alexsubALTlem3  23416  alexsubALTlem4  23417  alexsubALT  23418  metcnp3  23912  aalioulem3  25710  brbtwn2  27896  hial0  30086  hial02  30087  ococss  30277  lnopmi  30984  adjlnop  31070  pjss2coi  31148  pj3cor1i  31193  strlem3a  31236  hstrlem3a  31244  mdbr3  31281  mdbr4  31282  dmdmd  31284  dmdbr3  31289  dmdbr4  31290  dmdbr5  31292  ssmd2  31296  mdslmd1i  31313  mdsymlem7  31393  cdj1i  31417  cdj3lem2b  31421  sat1el2xp  34030  fvineqsneu  35928  lub0N  37697  glb0N  37701  hlrelat2  37912  snatpsubN  38259  pmaple  38270  pclclN  38400  pclfinN  38409  pclfinclN  38459  ltrneq2  38657  trlval2  38672  trlord  39078  trintALT  43251  lindslinindsimp2  46630
  Copyright terms: Public domain W3C validator