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

Theorem 2exbii 1727
Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
2exbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2exbii  |-  ( E. x E. y ph  <->  E. x E. y ps )

Proof of Theorem 2exbii
StepHypRef Expression
1 2exbii.1 . . 3  |-  ( ph  <->  ps )
21exbii 1726 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1726 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  3exbii  1728  3exdistr  1847  eeeanv  2094  ee4anv  2095  cbvex4v  2139  2sb5rf  2300  sbel2x  2308  2exsb  2318  2mo2  2399  rexcomf  2936  reean  2943  ceqsex3v  3074  ceqsex4v  3075  ceqsex8v  3077  vtocl3  3089  copsexg  4687  opelopabsbALT  4710  opabn0  4732  rabxp  4876  elxp3  4890  elvv  4898  elvvv  4899  copsex2gb  4950  elcnv2  5017  cnvuni  5026  xpdifid  5271  coass  5361  fununi  5659  dfmpt3  5708  tpres  6133  dfoprab2  6356  dmoprab  6396  rnoprab  6398  mpt2mptx  6406  resoprab  6411  elrnmpt2res  6429  ov3  6452  ov6g  6453  uniuni  6619  oprabex3  6801  wfrlem4  7057  oeeu  7322  xpassen  7684  zorn2lem6  8949  ltresr  9582  axaddf  9587  axmulf  9588  hashfun  12650  hash2prb  12674  5oalem7  27394  mpt2mptxf  28355  eulerpartlemgvv  29282  bnj600  29802  bnj916  29816  bnj983  29834  bnj986  29837  bnj996  29838  bnj1021  29847  elima4  30492  brtxp2  30719  brpprod3a  30724  brpprod3b  30725  elfuns  30753  brcart  30770  brimg  30775  brapply  30776  brsuccf  30779  brrestrict  30787  dfrdg4  30789  ellines  30990  bj-cbvex4vv  31410  itg2addnclem3  32059  dalem20  33329  dvhopellsm  34756  diblsmopel  34810  pm11.52  36806  2exanali  36807  pm11.6  36812  pm11.7  36816  opelopab4  36988  stoweidlem35  38008  mpt2mptx2  40624
  Copyright terms: Public domain W3C validator