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

Theorem 2ralbidv 2530
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.)
Hypothesis
Ref Expression
2ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2ralbidv (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2ralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21ralbidv 2506 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 2506 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2484
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 1470  ax-gen 1472  ax-4 1533  ax-17 1549
This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489
This theorem is referenced by:  cbvral3v  2753  poeq1  4346  soeq1  4362  isoeq1  5870  isoeq2  5871  isoeq3  5872  fnmpoovd  6301  smoeq  6376  xpf1o  6941  tapeq1  7364  elinp  7587  cauappcvgpr  7775  seq3caopr2  10638  seqcaopr2g  10639  addcn2  11621  mulcn2  11623  sgrp1  13243  ismhm  13293  mhmex  13294  issubm  13304  isnsg  13538  nmznsg  13549  isghm  13579  iscmn  13629  ring1  13821  opprsubrngg  13973  issubrg3  14009  islmod  14053  lmodlema  14054  lsssetm  14118  islssmd  14121  islidlm  14241  ispsmet  14795  ismet  14816  isxmet  14817  addcncntoplem  15033  elcncf  15045  mpodvdsmulf1o  15462
  Copyright terms: Public domain W3C validator