Theorem 4exbidv 1923

Description: Formula-building rule for 4 existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.)

Hypothesis

Ref	Expression
4exbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
4exbidv	⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦   𝜑,𝑧   𝜑,𝑤

Allowed substitution hints:   𝜓(𝑥, 𝑦, 𝑧, 𝑤)   𝜒(𝑥, 𝑦, 𝑧, 𝑤)

Proof of Theorem 4exbidv

Step	Hyp	Ref	Expression
1		4exbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	2exbidv 1921	. 2 ⊢ (𝜑 → (∃𝑧∃𝑤𝜓 ↔ ∃𝑧∃𝑤𝜒))
3	2	2exbidv 1921	1 ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  ceqsex8v  2868  copsex4g  4387  opbrop  4854  ovi3  6226  brecop  6899  th3q  6914  dfplpq2  7722  dfmpq2  7723  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  mulnnnq0  7818  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114