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

Theorem 2exbii 1948
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 1947 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1947 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wex 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908
This theorem depends on definitions:  df-bi 199  df-ex 1879
This theorem is referenced by:  3exbii  1949  4exdistrv  2055  3exdistr  2059  eeeanv  2374  ee4anv  2375  2exsb  2383  cbvex4v  2435  2sb5rf  2585  sbel2x  2592  2mo2  2730  rexcomf  3307  reean  3316  ceqsex3v  3463  ceqsex4v  3464  ceqsex8v  3466  vtocl3  3478  copsexg  5178  opelopabsbALT  5212  opabn0  5234  elxp2  5370  rabxp  5391  elxp3  5406  elvv  5414  elvvv  5415  copsex2gb  5468  elcnv2  5536  cnvuni  5545  xpdifid  5807  coass  5899  fununi  6201  dfmpt3  6251  tpres  6727  dfoprab2  6966  dmoprab  7006  rnoprab  7008  mpt2mptx  7016  resoprab  7021  elrnmpt2res  7039  ov3  7062  ov6g  7063  uniuni  7236  oprabex3  7422  wfrlem4  7688  wfrlem4OLD  7689  oeeu  7955  xpassen  8329  zorn2lem6  9645  ltresr  10284  axaddf  10289  axmulf  10290  hashfun  13520  hash2prb  13550  5oalem7  29070  mpt2mptxf  30021  eulerpartlemgvv  30979  bnj600  31531  bnj916  31545  bnj983  31563  bnj986  31566  bnj996  31567  bnj1021  31576  elima4  32212  brtxp2  32522  brpprod3a  32527  brpprod3b  32528  elfuns  32556  brcart  32573  brimg  32578  brapply  32579  brsuccf  32582  brrestrict  32590  dfrdg4  32592  ellines  32793  bj-cbvex4vv  33273  cnfinltrel  33781  itg2addnclem3  34001  brxrn2  34680  dfxrn2  34681  ecxrn  34692  inxpxrn  34696  rnxrn  34699  dalem20  35763  dvhopellsm  37187  diblsmopel  37241  pm11.52  39421  2exanali  39422  pm11.6  39427  pm11.7  39431  opelopab4  39590  stoweidlem35  41040  mpt2mptx2  42974
  Copyright terms: Public domain W3C validator