MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2exbii Structured version   Visualization version   GIF version

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

Proof of Theorem 2exbii
StepHypRef Expression
1 2exbii.1 . . 3 (𝜑𝜓)
21exbii 1764 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1764 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  3exbii  1766  3exdistr  1910  eeeanv  2171  ee4anv  2172  cbvex4v  2277  2sb5rf  2439  sbel2x  2447  2exsb  2457  2mo2  2538  rexcomf  3078  reean  3085  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  vtocl3  3235  copsexg  4882  opelopabsbALT  4909  opabn0  4931  elxp2  5056  rabxp  5078  elxp3  5092  elvv  5100  elvvv  5101  copsex2gb  5153  elcnv2  5222  cnvuni  5231  xpdifid  5481  coass  5571  fununi  5878  dfmpt3  5927  tpres  6371  dfoprab2  6599  dmoprab  6639  rnoprab  6641  mpt2mptx  6649  resoprab  6654  elrnmpt2res  6672  ov3  6695  ov6g  6696  uniuni  6865  oprabex3  7048  wfrlem4  7305  oeeu  7570  xpassen  7939  zorn2lem6  9206  ltresr  9840  axaddf  9845  axmulf  9846  hashfun  13084  hash2prb  13111  5oalem7  27903  mpt2mptxf  28860  eulerpartlemgvv  29765  bnj600  30243  bnj916  30257  bnj983  30275  bnj986  30278  bnj996  30279  bnj1021  30288  elima4  30924  brtxp2  31158  brpprod3a  31163  brpprod3b  31164  elfuns  31192  brcart  31209  brimg  31214  brapply  31215  brsuccf  31218  brrestrict  31226  dfrdg4  31228  ellines  31429  bj-cbvex4vv  31930  itg2addnclem3  32633  dalem20  33997  dvhopellsm  35424  diblsmopel  35478  pm11.52  37608  2exanali  37609  pm11.6  37614  pm11.7  37618  opelopab4  37788  stoweidlem35  38928  mpt2mptx2  41906
  Copyright terms: Public domain W3C validator