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

Theorem 2exbidv 1868
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 1825 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1825 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wex 1492
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-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  3exbidv  1869  4exbidv  1870  cbvex4v  1930  ceqsex3v  2779  ceqsex4v  2780  copsexg  4244  euotd  4254  elopab  4258  elxpi  4642  relop  4777  cbvoprab3  5950  ov6g  6011  th3qlem1  6636  ltresr  7837  fisumcom2  11445  fprodcom2fi  11633
  Copyright terms: Public domain W3C validator