Theorem ndexe-P6 825

Description: Natural Deduction Form of Existential Quantifier Elimination.

Hypotheses

Ref	Expression
ndexe-P6.1	⊢ Ⅎ𝑦𝛾
ndexe-P6.2	⊢ Ⅎ𝑦𝜑
ndexe-P6.3	⊢ (𝛾 → Ⅎ𝑦𝜓)
ndexe-P6.4	⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))
ndexe-P6.5	⊢ (𝛾 → ∃𝑥𝜑)

Assertion

Ref	Expression
ndexe-P6	⊢ (𝛾 → 𝜓)

Distinct variable group:   𝑥,𝑦

Proof of Theorem ndexe-P6

Step	Hyp	Ref	Expression
1		ndexe-P6.5	. . 3 ⊢ (𝛾 → ∃𝑥𝜑)
2		ndexe-P6.2	. . . . 5 ⊢ Ⅎ𝑦𝜑
3	2	cbvexpsub-P6 769	. . . 4 ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
4	3	subimr-P3.40b.RC 328	. . 3 ⊢ ((𝛾 → ∃𝑥𝜑) ↔ (𝛾 → ∃𝑦[𝑦 / 𝑥]𝜑))
5	1, 4	bimpf-P4.RC 532	. 2 ⊢ (𝛾 → ∃𝑦[𝑦 / 𝑥]𝜑)
6		ndexe-P6.1	. . 3 ⊢ Ⅎ𝑦𝛾
7		ndexe-P6.3	. . 3 ⊢ (𝛾 → Ⅎ𝑦𝜓)
8		ndexe-P6.4	. . 3 ⊢ (𝛾 → ([𝑦 / 𝑥]𝜑 → 𝜓))
9	6, 7, 8	exiad-P6 824	. 2 ⊢ (𝛾 → (∃𝑦[𝑦 / 𝑥]𝜑 → 𝜓))
10	5, 9	ndime-P3.6 171	1 ⊢ (𝛾 → 𝜓)

Syntax hints:  term-obj 1   → wff-imp 10  ∃wff-exists 595  Ⅎwff-nfree 681  [wff-psub 714

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L10 27  ax-L11 28  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  ndexe-P7.20  845