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

Step	Hyp	Ref	Expression
1		3exbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	exbii 1849	. 2 ⊢ (∃𝑧𝜑 ↔ ∃𝑧𝜓)
3	2	2exbii 1850	1 ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)

Syntax hints:   ↔ wb 206  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  4exdistr  1962  ceqsex6v  3497  oprabidw  7389  oprabid  7390  dfoprab2  7416  dftpos3  8186  xpassen  8999  hash3tpb  14418  bnj916  35089  bnj917  35090  bnj983  35107  bnj996  35112  bnj1021  35122  bnj1033  35125  ellines  36346  rnxrn  38616  ichexmpl1  47725