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

Theorem 2ralbidv 2459
 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 2437 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 2437 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2416 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 1423  ax-gen 1425  ax-4 1487  ax-17 1506 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421 This theorem is referenced by:  cbvral3v  2667  poeq1  4221  soeq1  4237  isoeq1  5702  isoeq2  5703  isoeq3  5704  fnmpoovd  6112  smoeq  6187  xpf1o  6738  elinp  7289  cauappcvgpr  7477  seq3caopr2  10262  addcn2  11086  mulcn2  11088  ispsmet  12502  ismet  12523  isxmet  12524  addcncntoplem  12730  elcncf  12739
 Copyright terms: Public domain W3C validator