Theorem 3exbii 1850

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

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

This theorem is referenced by:  4exdistr  1961  ceqsex6v  3494  oprabidw  7380  oprabid  7381  dfoprab2  7407  dftpos3  8177  xpassen  8988  hash3tpb  14402  bnj916  34900  bnj917  34901  bnj983  34918  bnj996  34923  bnj1021  34933  bnj1033  34936  ellines  36130  rnxrn  38374  ichexmpl1  47457