Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rexbii 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
Assertion
Ref Expression
2rexbii

Proof of Theorem 2rexbii
StepHypRef Expression
1 rexbii.1 . . 3
21rexbii 2959 . 2
32rexbii 2959 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  E.wrex 2808 This theorem is referenced by:  3reeanv  3026  addcompr  9420  mulcompr  9422  4fvwrd4  11822  ntrivcvgmul  13711  prodmo  13743  pythagtriplem2  14341  pythagtrip  14358  isnsgrp  15915  efgrelexlemb  16768  ordthaus  19885  regr1lem2  20241  fmucndlem  20794  axpasch  24244  axeuclid  24266  axcontlem4  24270  frgrawopreglem5  25048  xrofsup  27582  poseq  29333  altopelaltxp  29626  brsegle  29758  mzpcompact2lem  30684  sbc4rex  30722  7rexfrabdioph  30733  expdiophlem1  30963  ralnex2  31435  fourierdlem42  31931  ldepslinc  33110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-rex 2813
 Copyright terms: Public domain W3C validator