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

Theorem 2exbii 1852
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 1851 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1851 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  3exbii  1853  2exanali  1864  4exdistrv  1961  3exdistr  1965  cbvex4vw  2046  eeeanv  2347  ee4anv  2348  2exsb  2357  cbvex4v  2414  2sb5rf  2471  sbel2x  2473  2mo2  2648  reeanlem  3219  rexcomf  3289  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  copsexgw  5452  copsexg  5453  copsex2g  5455  vopelopabsb  5491  opabn0  5515  elxp2  5662  rabxp  5685  elxp3  5703  elvv  5711  elvvv  5712  copsex2gb  5767  elcnv2  5838  cnvuni  5847  xpdifid  6125  coass  6222  fununi  6581  dfmpt3  6640  tpres  7155  dfoprab2  7420  dmoprab  7463  rnoprab  7465  mpomptx  7474  resoprab  7479  elrnmpores  7498  ov3  7522  ov6g  7523  uniuni  7701  opabex3rd  7904  oprabex3  7915  wfrlem4OLD  8263  oeeu  8555  xpassen  9017  sbthfilem  9152  zorn2lem6  10444  ltresr  11083  axaddf  11088  axmulf  11089  hashfun  14344  hash2prb  14378  5oalem7  30644  mpomptxf  31639  eulerpartlemgvv  33016  bnj600  33571  bnj916  33585  bnj983  33603  bnj986  33607  bnj996  33608  bnj1021  33618  dfacycgr1  33778  satfv1  33997  elima4  34389  brtxp2  34495  brpprod3a  34500  brpprod3b  34501  elfuns  34529  brcart  34546  brimg  34551  brapply  34552  brsuccf  34555  brrestrict  34563  dfrdg4  34565  ellines  34766  bj-cbvex4vv  35299  itg2addnclem3  36160  brxrn2  36866  dfxrn2  36867  ecxrn  36878  inxpxrn  36886  rnxrn  36889  dalem20  38185  dvhopellsm  39609  diblsmopel  39663  ralopabb  41757  en2pr  41893  pm11.52  42741  pm11.6  42746  pm11.7  42750  opelopab4  42907  stoweidlem35  44350  fundcmpsurbijinj  45676  mpomptx2  46484
  Copyright terms: Public domain W3C validator