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

Theorem 2rexbii 3230
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 3229 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3229 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-rex 3102
This theorem is referenced by:  rexnal3  3232  ralnex2  3233  ralnex3  3234  3reeanv  3296  addcompr  10128  mulcompr  10130  4fvwrd4  12683  ntrivcvgmul  14855  prodmo  14887  pythagtriplem2  15739  pythagtrip  15756  isnsgrp  17493  efgrelexlemb  18364  ordthaus  21402  regr1lem2  21757  fmucndlem  22308  dfcgra2  25935  axpasch  26035  axeuclid  26057  axcontlem4  26061  umgr2edg1  26318  wwlksnwwlksnon  27053  xrofsup  29860  poseq  32074  madeval2  32257  altopelaltxp  32404  brsegle  32536  mzpcompact2lem  37816  sbc4rex  37855  7rexfrabdioph  37866  expdiophlem1  38089  fourierdlem42  40845  ldepslinc  42866
  Copyright terms: Public domain W3C validator