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

Theorem ralrimivv 2472
 Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
Hypothesis
Ref Expression
ralrimivv.1 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
Assertion
Ref Expression
ralrimivv (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Distinct variable groups:   𝑥,𝑦,𝜑   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivv
StepHypRef Expression
1 ralrimivv.1 . . . 4 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
21expd 256 . . 3 (𝜑 → (𝑥𝐴 → (𝑦𝐵𝜓)))
32ralrimdv 2470 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2463 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  ∀wral 2375 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 1391  ax-gen 1393  ax-4 1455  ax-17 1474 This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380 This theorem is referenced by:  ralrimivva  2473  ralrimdvv  2475  reuind  2842  ssrel2  4567  f1o2ndf1  6055  smoiso  6129  nndifsnid  6333  receuap  8291  lbreu  8561  tgcl  12015  topbas  12018  epttop  12041  restbasg  12119  txbas  12208  txbasval  12217  blfps  12337  blf  12338  blbas  12361
 Copyright terms: Public domain W3C validator