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

Theorem 3exbii 1841
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 1839 . 2 (∃𝑧𝜑 ↔ ∃𝑧𝜓)
322exbii 1840 1 (∃𝑥𝑦𝑧𝜑 ↔ ∃𝑥𝑦𝑧𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  4exdistr  1954  ceqsex6v  3545  oprabidw  7176  oprabid  7177  dfoprab2  7201  dftpos3  7899  xpassen  8599  bnj916  32104  bnj917  32105  bnj983  32122  bnj996  32126  bnj1021  32135  bnj1033  32138  ellines  33510  rnxrn  35526  ichexmpl1  43508
  Copyright terms: Public domain W3C validator