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

Theorem ralrimi 2506
 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 1503 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 2422 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 133 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1330  Ⅎwnf 1437   ∈ 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 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422 This theorem is referenced by:  ralrimiv  2507  reximdai  2533  r19.12  2541  rexlimd  2549  rexlimd2  2550  r19.29af2  2575  r19.37  2586  ralidm  3466  iineq2d  3839  mpteq2da  4023  onintonm  4439  mpteqb  5517  fmptdf  5583  eusvobj2  5766  tfri3  6270  mapxpen  6748  fodjuomnilemdc  7022  cc3  7098  fimaxre2  11028  zsupcllemstep  11667  bezoutlemmain  11715  bezoutlemzz  11719  exmidunben  11968  mulcncf  12792  limccnp2lem  12846
 Copyright terms: Public domain W3C validator