Theorem 3exbii 1857

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

Syntax hints:   ↔ wb 207  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  4exdistr  1968  ceqsex6v  3486  oprabidw  7387  oprabid  7388  dfoprab2  7414  dftpos3  8184  xpassen  8999  hash3tpb  14448  bnj916  35115  bnj917  35116  bnj983  35133  bnj996  35138  bnj1021  35148  bnj1033  35151  ellines  36380  rnxrn  38788  ichexmpl1  47944