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

Theorem 2ralbidv 2529
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 2505 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 2505 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2483
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 1469  ax-gen 1471  ax-4 1532  ax-17 1548
This theorem depends on definitions:  df-bi 117  df-nf 1483  df-ral 2488
This theorem is referenced by:  cbvral3v  2752  poeq1  4345  soeq1  4361  isoeq1  5869  isoeq2  5870  isoeq3  5871  fnmpoovd  6300  smoeq  6375  xpf1o  6940  tapeq1  7363  elinp  7586  cauappcvgpr  7774  seq3caopr2  10636  seqcaopr2g  10637  addcn2  11592  mulcn2  11594  sgrp1  13214  ismhm  13264  mhmex  13265  issubm  13275  isnsg  13509  nmznsg  13520  isghm  13550  iscmn  13600  ring1  13792  opprsubrngg  13944  issubrg3  13980  islmod  14024  lmodlema  14025  lsssetm  14089  islssmd  14092  islidlm  14212  ispsmet  14766  ismet  14787  isxmet  14788  addcncntoplem  15004  elcncf  15016  mpodvdsmulf1o  15433
  Copyright terms: Public domain W3C validator