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

Theorem ralrimivv 2551
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 2549 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2542 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 2141  wral 2448
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  ralrimivva  2552  ralrimdvv  2554  reuind  2935  ssrel2  4699  f1o2ndf1  6204  smoiso  6278  nndifsnid  6483  receuap  8574  lbreu  8848  0subm  12688  insubm  12689  tgcl  12779  topbas  12782  epttop  12805  restbasg  12883  txbas  12973  txbasval  12982  blfps  13124  blf  13125  blbas  13148
  Copyright terms: Public domain W3C validator