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

Theorem 2ralbidv 2514
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 2490 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32ralbidv 2490 1 (𝜑 → (∀𝑥𝐴𝑦𝐵 𝜓 ↔ ∀𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2468
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 1458  ax-gen 1460  ax-4 1521  ax-17 1537
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473
This theorem is referenced by:  cbvral3v  2733  poeq1  4317  soeq1  4333  isoeq1  5822  isoeq2  5823  isoeq3  5824  fnmpoovd  6239  smoeq  6314  xpf1o  6871  tapeq1  7280  elinp  7502  cauappcvgpr  7690  seq3caopr2  10512  addcn2  11349  mulcn2  11351  sgrp1  12871  ismhm  12910  mhmex  12911  issubm  12921  isnsg  13138  nmznsg  13149  isghm  13179  iscmn  13229  ring1  13408  opprsubrngg  13555  issubrg3  13591  islmod  13604  lmodlema  13605  lsssetm  13669  islssmd  13672  islidlm  13792  ispsmet  14275  ismet  14296  isxmet  14297  addcncntoplem  14503  elcncf  14512
  Copyright terms: Public domain W3C validator