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

Theorem 2exbidv 1840
 Description: Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2exbidv (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3 (𝜑 → (𝜓𝜒))
21exbidv 1797 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1797 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∃wex 1468 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-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3exbidv  1841  4exbidv  1842  cbvex4v  1900  ceqsex3v  2723  ceqsex4v  2724  copsexg  4161  euotd  4171  elopab  4175  elxpi  4550  relop  4684  cbvoprab3  5840  ov6g  5901  th3qlem1  6524  ltresr  7640  fisumcom2  11200
 Copyright terms: Public domain W3C validator