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

Theorem 2rexbii 2889
 Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
rexbii.1
Assertion
Ref Expression
2rexbii

Proof of Theorem 2rexbii
StepHypRef Expression
1 rexbii.1 . . 3
21rexbii 2888 . 2
32rexbii 2888 1
 Colors of variables: wff setvar class Syntax hints:   wb 188  wrex 2737 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681 This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-rex 2742 This theorem is referenced by:  ralnex2  2892  ralnex3  2893  3reeanv  2958  addcompr  9443  mulcompr  9445  4fvwrd4  11906  ntrivcvgmul  13951  prodmo  13983  pythagtriplem2  14760  pythagtrip  14777  isnsgrp  16524  efgrelexlemb  17393  ordthaus  20393  regr1lem2  20748  fmucndlem  21299  dfcgra2  24864  axpasch  24964  axeuclid  24986  axcontlem4  24990  frgrawopreglem5  25769  xrofsup  28346  poseq  30484  altopelaltxp  30736  brsegle  30868  mzpcompact2lem  35587  sbc4rex  35626  7rexfrabdioph  35637  expdiophlem1  35870  fourierdlem42  38006  fourierdlem42OLD  38007  usgr2edg1  39278  ldepslinc  40289
 Copyright terms: Public domain W3C validator