Theorem 3exbii 1848

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 1846	. 2 ⊢ (∃𝑧𝜑 ↔ ∃𝑧𝜓)
3	2	2exbii 1847	1 ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓)

Syntax hints:   ↔ wb 206  ∃wex 1777

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

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

This theorem is referenced by:  4exdistr  1961  ceqsex6v  3551  oprabidw  7479  oprabid  7480  dfoprab2  7508  dftpos3  8285  xpassen  9132  hash3tpb  14544  bnj916  34909  bnj917  34910  bnj983  34927  bnj996  34932  bnj1021  34942  bnj1033  34945  ellines  36116  rnxrn  38354  ichexmpl1  47343