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

Theorem 2ralbidv 2501
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 2477 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 2477 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  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:  cbvral3v  2719  poeq1  4300  soeq1  4316  isoeq1  5802  isoeq2  5803  isoeq3  5804  fnmpoovd  6216  smoeq  6291  xpf1o  6844  tapeq1  7251  elinp  7473  cauappcvgpr  7661  seq3caopr2  10482  addcn2  11318  mulcn2  11320  sgrp1  12816  ismhm  12853  issubm  12863  isnsg  13062  nmznsg  13073  iscmn  13096  ring1  13236  issubrg3  13368  islmod  13381  lmodlema  13382  ispsmet  13826  ismet  13847  isxmet  13848  addcncntoplem  14054  elcncf  14063
  Copyright terms: Public domain W3C validator