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

Theorem 2rexbii 2960
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
rexbii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
2rexbii  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x  e.  A  E. y  e.  B  ps )

Proof of Theorem 2rexbii
StepHypRef Expression
1 rexbii.1 . . 3  |-  ( ph  <->  ps )
21rexbii 2959 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2959 1  |-  ( E. x  e.  A  E. y  e.  B  ph  <->  E. x  e.  A  E. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wrex 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-rex 2813
This theorem is referenced by:  3reeanv  3026  addcompr  9416  mulcompr  9418  4fvwrd4  11819  ntrivcvgmul  13723  prodmo  13755  pythagtriplem2  14353  pythagtrip  14370  isnsgrp  16042  efgrelexlemb  16895  ordthaus  20012  regr1lem2  20367  fmucndlem  20920  axpasch  24371  axeuclid  24393  axcontlem4  24397  frgrawopreglem5  25175  xrofsup  27742  poseq  29550  altopelaltxp  29831  brsegle  29963  mzpcompact2lem  30889  sbc4rex  30927  7rexfrabdioph  30938  expdiophlem1  31167  ralnex2  31638  fourierdlem42  32134  ldepslinc  33254
  Copyright terms: Public domain W3C validator