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

Theorem 3exbii 1851
 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 1849 . 2 (∃𝑧𝜑 ↔ ∃𝑧𝜓)
322exbii 1850 1 (∃𝑥𝑦𝑧𝜑 ↔ ∃𝑥𝑦𝑧𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∃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 210  df-ex 1782 This theorem is referenced by:  4exdistr  1963  ceqsex6v  3522  oprabidw  7171  oprabid  7172  dfoprab2  7196  dftpos3  7897  xpassen  8598  bnj916  32279  bnj917  32280  bnj983  32297  bnj996  32302  bnj1021  32312  bnj1033  32315  ellines  33687  rnxrn  35764  ichexmpl1  43925
 Copyright terms: Public domain W3C validator