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

Theorem 2rexbii 2966
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 2965 . 2  |-  ( E. y  e.  B  ph  <->  E. y  e.  B  ps )
32rexbii 2965 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 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820
This theorem is referenced by:  3reeanv  3030  addcompr  9399  mulcompr  9401  4fvwrd4  11790  pythagtriplem2  14200  pythagtrip  14217  efgrelexlemb  16574  ordthaus  19679  regr1lem2  20004  fmucndlem  20557  axpasch  23948  axeuclid  23970  axcontlem4  23974  frgrawopreglem5  24753  xrofsup  27278  ntrivcvgmul  28641  prodmo  28673  poseq  28938  altopelaltxp  29231  brsegle  29363  mzpcompact2lem  30316  sbc4rex  30354  7rexfrabdioph  30365  expdiophlem1  30595  ralnex2  31045  fourierdlem42  31477  ldepslinc  32209
  Copyright terms: Public domain W3C validator