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

Theorem 2exbii 1573
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 1572 . 2  |-  ( E. y ph  <->  E. y ps )
32exbii 1572 1  |-  ( E. x E. y ph  <->  E. x E. y ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531
This theorem is referenced by:  3exbii  1574  3exdistr  1863  ee4anv  1868  cbvex4v  1965  sbel2x  2077  2eu4  2239  2eu6  2241  rexcomf  2712  reean  2719  ceqsex3v  2839  ceqsex4v  2840  ceqsex8v  2842  vtocl3  2853  copsexg  4268  opelopabsbOLD  4289  opabn0  4311  uniuni  4543  rabxp  4741  elxp3  4755  elvv  4764  elvvv  4765  elcnv2  4875  cnvuni  4882  coass  5207  fununi  5332  dfmpt3  5382  dfoprab2  5911  dmoprab  5944  rnoprab  5946  mpt2mptx  5954  resoprab  5956  oprabex3  5978  ov3  6000  ov6g  6001  copsex2gb  6196  oeeu  6617  xpassen  6972  zorn2lem6  8144  ltresr  8778  axaddf  8783  axmulf  8784  hashfun  11405  5oalem7  22255  wfrlem4  24330  brtxp2  24492  brpprod3a  24497  brpprod3b  24498  elfuns  24525  brcart  24542  brimg  24547  brapply  24548  brsuccf  24551  brrestrict  24559  dfrdg4  24560  ellines  24847  itg2addnc  25005  dfoprab4pop  25140  pm11.52  27688  2exanali  27689  pm11.6  27694  pm11.7  27698  stoweidlem35  27887  opelopab4  28616  bnj600  29267  bnj916  29281  bnj983  29299  bnj986  29302  bnj996  29303  bnj1021  29312  sbel2xNEW7  29586  ee4anvOLD7  29659  cbvex4vOLD7  29692  dalem20  30504  dvhopellsm  31929  diblsmopel  31983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator