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

Theorem 2exbii 1683
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 1682 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1682 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646
This theorem depends on definitions:  df-bi 185  df-ex 1628
This theorem is referenced by:  3exbii  1684  3exdistr  1798  eeeanv  2007  ee4anv  2008  cbvex4v  2050  2sb5rf  2209  sbel2x  2217  2exsb  2227  2mo2  2313  2moOLD  2315  2eu4OLD  2322  2eu6OLD  2325  rexcomf  2955  reean  2962  ceqsex3v  3087  ceqsex4v  3088  ceqsex8v  3090  vtocl3  3101  copsexg  4660  opelopabsbALT  4683  opabn0  4705  rabxp  4963  elxp3  4977  elvv  4985  elvvv  4986  copsex2gb  5039  elcnv2  5106  cnvuni  5115  xpdifid  5358  coass  5447  fununi  5575  dfmpt3  5624  tpres  6040  dfoprab2  6260  dmoprab  6300  rnoprab  6302  mpt2mptx  6310  resoprab  6315  elrnmpt2res  6333  ov3  6356  ov6g  6357  uniuni  6526  oprabex3  6706  oeeu  7188  xpassen  7548  zorn2lem6  8812  ltresr  9446  axaddf  9451  axmulf  9452  hashfun  12418  5oalem7  26716  mpt2mptxf  27695  eulerpartlemgvv  28534  elima4  29410  wfrlem4  29547  brtxp2  29720  brpprod3a  29725  brpprod3b  29726  elfuns  29754  brcart  29771  brimg  29776  brapply  29777  brsuccf  29780  brrestrict  29788  dfrdg4  29789  ellines  29991  itg2addnclem3  30270  pm11.52  31496  2exanali  31497  pm11.6  31502  pm11.7  31506  stoweidlem35  32018  mpt2mptx2  33159  opelopab4  33699  bnj600  34359  bnj916  34373  bnj983  34391  bnj986  34394  bnj996  34395  bnj1021  34404  bj-cbvex4vv  34690  dalem20  35865  dvhopellsm  37292  diblsmopel  37346
  Copyright terms: Public domain W3C validator