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

Theorem ralrimiv 2507
 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 1509 . 2 𝑥𝜑
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2ralrimi 2506 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1481  ∀wral 2417 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422 This theorem is referenced by:  ralrimiva  2508  ralrimivw  2509  ralrimivv  2516  r19.27av  2570  rr19.3v  2827  rabssdv  3182  rzal  3465  trin  4044  class2seteq  4095  ralxfrALT  4396  ssorduni  4411  ordsucim  4424  onintonm  4441  issref  4929  funimaexglem  5214  resflem  5592  poxp  6137  rdgss  6288  dom2lem  6674  supisoti  6905  ordiso2  6928  updjud  6975  uzind  9186  zindd  9193  lbzbi  9435  icoshftf1o  9804  maxabslemval  11012  xrmaxiflemval  11051  fisum0diag2  11248  alzdvds  11588  hashgcdeq  11940  tgcl  12272  distop  12293  neiuni  12369  cnpnei  12427  isxmetd  12555  fsumcncntop  12764  bj-nntrans2  13321  bj-inf2vnlem1  13339
 Copyright terms: Public domain W3C validator