Theorem 3exbii 1882

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

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

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

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

This theorem is used by:  4exdistr  1995  ceqsex6v  3507  cotsexgw  5466  oprabidw  7458  oprabid  7459  dfoprab2  7485  funmpt3  7694  mpt3fvd  7695  dftpos3  8272  xpassen  9101  hash3tpb  14650  bnj916  35616  bnj917  35617  bnj983  35634  bnj996  35639  bnj1021  35649  bnj1033  35652  ellines  37044  rnxrn  39493  ichexmpl1  48690