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

Theorem 2exbii 1497
Description: Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
exbii.1 (𝜑𝜓)
Assertion
Ref Expression
2exbii (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)

Proof of Theorem 2exbii
StepHypRef Expression
1 exbii.1 . . 3 (𝜑𝜓)
21exbii 1496 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1496 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff set class
Syntax hints:  wb 98  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3exbii  1498  19.42vvvv  1790  3exdistr  1792  cbvex4v  1805  ee4anv  1809  ee8anv  1810  sbel2x  1874  2eu4  1993  rexcomf  2472  reean  2478  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  copsexg  3981  opelopabsbALT  3996  opabm  4017  uniuni  4183  rabxp  4380  elxp3  4394  elvv  4402  elvvv  4403  rexiunxp  4478  elcnv2  4513  cnvuni  4521  coass  4839  fununi  4967  dfmpt3  5021  dfoprab2  5552  dmoprab  5585  rnoprab  5587  mpt2mptx  5595  resoprab  5597  ovi3  5637  ov6g  5638  oprabex3  5756  xpassen  6304  enq0enq  6529  enq0sym  6530  enq0tr  6532  ltresr  6915
  Copyright terms: Public domain W3C validator