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

Theorem 3exbii 1852
Description: Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
Hypothesis
Ref Expression
3exbii.1 (𝜑𝜓)
Assertion
Ref Expression
3exbii (∃𝑥𝑦𝑧𝜑 ↔ ∃𝑥𝑦𝑧𝜓)

Proof of Theorem 3exbii
StepHypRef Expression
1 3exbii.1 . . 3 (𝜑𝜓)
21exbii 1850 . 2 (∃𝑧𝜑 ↔ ∃𝑧𝜓)
322exbii 1851 1 (∃𝑥𝑦𝑧𝜑 ↔ ∃𝑥𝑦𝑧𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  4exdistr  1965  ceqsex6v  3500  oprabidw  7382  oprabid  7383  dfoprab2  7409  dftpos3  8167  xpassen  8968  bnj916  33357  bnj917  33358  bnj983  33375  bnj996  33380  bnj1021  33390  bnj1033  33393  ellines  34675  rnxrn  36798  ichexmpl1  45562
  Copyright terms: Public domain W3C validator