ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimiv GIF version

Theorem ralrimiv 2478
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
Hypothesis
Ref Expression
ralrimiv.1 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
ralrimiv (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiv
StepHypRef Expression
1 nfv 1491 . 2 𝑥𝜑
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2ralrimi 2477 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1463  wral 2390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2395
This theorem is referenced by:  ralrimiva  2479  ralrimivw  2480  ralrimivv  2487  r19.27av  2541  rr19.3v  2793  rabssdv  3143  rzal  3426  trin  3996  class2seteq  4047  ralxfrALT  4348  ssorduni  4363  ordsucim  4376  onintonm  4393  issref  4879  funimaexglem  5164  resflem  5538  poxp  6083  rdgss  6234  dom2lem  6620  supisoti  6849  ordiso2  6872  updjud  6919  uzind  9066  zindd  9073  lbzbi  9310  icoshftf1o  9667  maxabslemval  10872  xrmaxiflemval  10911  fisum0diag2  11108  alzdvds  11400  hashgcdeq  11749  tgcl  12076  distop  12097  neiuni  12173  cnpnei  12230  isxmetd  12336  fsumcncntop  12542  bj-nntrans2  12840  bj-inf2vnlem1  12858
  Copyright terms: Public domain W3C validator