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

Theorem 2exbii 1772
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 1771 . 2 (∃𝑦𝜑 ↔ ∃𝑦𝜓)
32exbii 1771 1 (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  3exbii  1773  3exdistr  1920  eeeanv  2182  ee4anv  2183  cbvex4v  2288  2sb5rf  2450  sbel2x  2458  2exsb  2468  2mo2  2549  rexcomf  3090  reean  3099  ceqsex3v  3235  ceqsex4v  3236  ceqsex8v  3238  vtocl3  3251  copsexg  4921  opelopabsbALT  4949  opabn0  4971  elxp2  5097  rabxp  5119  elxp3  5135  elvv  5143  elvvv  5144  copsex2gb  5196  elcnv2  5265  cnvuni  5274  xpdifid  5526  coass  5618  fununi  5927  dfmpt3  5976  tpres  6426  dfoprab2  6661  dmoprab  6701  rnoprab  6703  mpt2mptx  6711  resoprab  6716  elrnmpt2res  6734  ov3  6757  ov6g  6758  uniuni  6927  oprabex3  7109  wfrlem4  7370  oeeu  7635  xpassen  8006  zorn2lem6  9275  ltresr  9913  axaddf  9918  axmulf  9919  hashfun  13172  hash2prb  13200  5oalem7  28389  mpt2mptxf  29343  eulerpartlemgvv  30243  bnj600  30732  bnj916  30746  bnj983  30764  bnj986  30767  bnj996  30768  bnj1021  30777  elima4  31416  brtxp2  31665  brpprod3a  31670  brpprod3b  31671  elfuns  31699  brcart  31716  brimg  31721  brapply  31722  brsuccf  31725  brrestrict  31733  dfrdg4  31735  ellines  31936  bj-cbvex4vv  32420  itg2addnclem3  33130  dalem20  34494  dvhopellsm  35921  diblsmopel  35975  pm11.52  38103  2exanali  38104  pm11.6  38109  pm11.7  38113  opelopab4  38284  stoweidlem35  39585  mpt2mptx2  41427
  Copyright terms: Public domain W3C validator