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

Theorem 2rexbii 3180
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 3179 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3179 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-rex 3056
This theorem is referenced by:  rexnal3  3182  ralnex2  3183  ralnex3  3184  3reeanv  3246  addcompr  10035  mulcompr  10037  4fvwrd4  12653  ntrivcvgmul  14833  prodmo  14865  pythagtriplem2  15724  pythagtrip  15741  isnsgrp  17489  efgrelexlemb  18363  ordthaus  21390  regr1lem2  21745  fmucndlem  22296  dfcgra2  25920  axpasch  26020  axeuclid  26042  axcontlem4  26046  umgr2edg1  26302  wwlksnwwlksnon  27033  xrofsup  29842  poseq  32059  madeval2  32242  altopelaltxp  32389  brsegle  32521  mzpcompact2lem  37816  sbc4rex  37855  7rexfrabdioph  37866  expdiophlem1  38090  fourierdlem42  40869  ldepslinc  42808
  Copyright terms: Public domain W3C validator