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

Theorem ralrimiv 2391
 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 1421 . 2 𝑥𝜑
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2ralrimi 2390 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  ∀wral 2306 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311 This theorem is referenced by:  ralrimiva  2392  ralrimivw  2393  ralrimivv  2400  r19.27av  2448  rr19.3v  2682  rabssdv  3020  rzal  3318  trin  3864  class2seteq  3916  ralxfrALT  4199  ssorduni  4213  ordsucim  4226  onintonm  4243  issref  4707  funimaexglem  4982  poxp  5853  rdgss  5970  dom2lem  6252  ordiso2  6357  uzind  8349  zindd  8356  lbzbi  8551  icoshftf1o  8859  bj-nntrans2  10077  bj-inf2vnlem1  10095
 Copyright terms: Public domain W3C validator