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

Theorem ralrimi 2433
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
Hypotheses
Ref Expression
ralrimi.1 𝑥𝜑
ralrimi.2 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
ralrimi (𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3 𝑥𝜑
2 ralrimi.2 . . 3 (𝜑 → (𝑥𝐴𝜓))
31, 2alrimi 1456 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2354 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 132 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1283  Ⅎwnf 1390   ∈ wcel 1434  ∀wral 2349 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354 This theorem is referenced by:  ralrimiv  2434  reximdai  2460  r19.12  2467  rexlimd  2475  rexlimd2  2476  r19.29af2  2497  r19.37  2507  ralidm  3349  iineq2d  3706  mpteq2da  3875  onintonm  4269  mpteqb  5293  eusvobj2  5529  tfri3  6016  fimaxre2  10247  zsupcllemstep  10485  bezoutlemmain  10531  bezoutlemzz  10535
 Copyright terms: Public domain W3C validator