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

Theorem 2exbii 1842
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 1841 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1841 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  3exbii  1843  2exanali  1853  4exdistrv  1950  3exdistr  1955  cbvex4vw  2042  eeeanv  2365  ee4anv  2366  2exsb  2374  cbvex4v  2433  2sb5rf  2493  sbel2x  2496  2mo2  2730  rexcomOLD  3360  rexcomf  3362  reeanlem  3370  ceqsex3v  3550  ceqsex4v  3551  ceqsex8v  3553  copsexgw  5377  copsexg  5378  opelopabsbALT  5412  opabn0  5436  elxp2  5577  rabxp  5598  elxp3  5616  elvv  5624  elvvv  5625  copsex2gb  5677  elcnv2  5746  cnvuni  5755  xpdifid  6022  coass  6115  fununi  6425  dfmpt3  6478  tpres  6962  dfoprab2  7207  dmoprab  7248  rnoprab  7250  mpomptx  7258  resoprab  7263  elrnmpores  7281  ov3  7304  ov6g  7305  uniuni  7476  opabex3rd  7661  oprabex3  7672  wfrlem4  7952  oeeu  8222  xpassen  8603  zorn2lem6  9915  ltresr  10554  axaddf  10559  axmulf  10560  hashfun  13791  hash2prb  13823  5oalem7  29351  mpomptxf  30340  eulerpartlemgvv  31520  bnj600  32077  bnj916  32091  bnj983  32109  bnj986  32112  bnj996  32113  bnj1021  32122  dfacycgr1  32275  satfv1  32494  elima4  32903  brtxp2  33226  brpprod3a  33231  brpprod3b  33232  elfuns  33260  brcart  33277  brimg  33282  brapply  33283  brsuccf  33286  brrestrict  33294  dfrdg4  33296  ellines  33497  bj-cbvex4vv  34011  itg2addnclem3  34812  brxrn2  35494  dfxrn2  35495  ecxrn  35506  inxpxrn  35510  rnxrn  35513  dalem20  36696  dvhopellsm  38120  diblsmopel  38174  en2pr  39767  pm11.52  40580  pm11.6  40585  pm11.7  40589  opelopab4  40746  stoweidlem35  42182  mpomptx2  44211
  Copyright terms: Public domain W3C validator