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

Theorem ralrimdv 2950
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 443 . . 3 ((𝜑𝜓) → (𝑥𝐴𝜒))
32ralrimiv 2947 . 2 ((𝜑𝜓) → ∀𝑥𝐴 𝜒)
43ex 448 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ral 2900
This theorem is referenced by:  ralrimdva  2951  ralrimivv  2952  wefrc  5022  oneqmin  6875  nneneq  8006  cflm  8933  coflim  8944  isf32lem12  9047  axdc3lem2  9134  zorn2lem7  9185  axpre-sup  9847  zmax  11620  zbtwnre  11621  supxrunb2  11981  fzrevral  12252  islss4  18732  topbas  20535  elcls3  20645  neips  20675  clslp  20710  subbascn  20816  cnpnei  20826  comppfsc  21093  fgss2  21436  fbflim2  21539  alexsubALTlem3  21611  alexsubALTlem4  21612  alexsubALT  21613  metcnp3  22103  aalioulem3  23838  brbtwn2  25531  hial0  27177  hial02  27178  ococss  27370  lnopmi  28077  adjlnop  28163  pjss2coi  28241  pj3cor1i  28286  strlem3a  28329  hstrlem3a  28337  mdbr3  28374  mdbr4  28375  dmdmd  28377  dmdbr3  28382  dmdbr4  28383  dmdbr5  28385  ssmd2  28389  mdslmd1i  28406  mdsymlem7  28486  cdj1i  28510  cdj3lem2b  28514  lub0N  33318  glb0N  33322  hlrelat2  33531  snatpsubN  33878  pmaple  33889  pclclN  34019  pclfinN  34028  pclfinclN  34078  ltrneq2  34276  trlval2  34292  trlord  34699  trintALT  37963  lindslinindsimp2  42068
  Copyright terms: Public domain W3C validator