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

Theorem ralrimivv 2558
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 258 . . 3 (𝜑 → (𝑥𝐴 → (𝑦𝐵𝜓)))
32ralrimdv 2556 . 2 (𝜑 → (𝑥𝐴 → ∀𝑦𝐵 𝜓))
43ralrimiv 2549 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  ralrimivva  2559  ralrimdvv  2561  reuind  2943  ssrel2  4717  f1o2ndf1  6229  smoiso  6303  nndifsnid  6508  receuap  8626  lbreu  8902  0subm  12871  insubm  12872  iscmnd  13101  tgcl  13567  topbas  13570  epttop  13593  restbasg  13671  txbas  13761  txbasval  13770  blfps  13912  blf  13913  blbas  13936
  Copyright terms: Public domain W3C validator