Theorem 3exbii 1883

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  4exdistr  1996  ceqsex6v  3508  cotsexgw  5470  oprabidw  7482  oprabid  7483  dfoprab2  7509  funmpt3  7719  mpt3fvd  7720  dftpos3  8299  xpassen  9128  hash3tpb  14681  bnj916  35674  bnj917  35675  bnj983  35692  bnj996  35697  bnj1021  35707  bnj1033  35710  ellines  37132  rnxrn  39619  ichexmpl1  48824