Theorem qimeqex-P7-L2 1055

Description: Lemma for qimeqex-P7 1056. †

Assertion

Ref	Expression
qimeqex-P7-L2	⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem qimeqex-P7-L2

Step	Hyp	Ref	Expression
1		ndnfrex1-P7.8 833	. . . 4 ⊢ Ⅎ𝑥∃𝑥(𝜑 → 𝜓)
2		ndnfrall1-P7.7 832	. . . 4 ⊢ Ⅎ𝑥∀𝑥𝜑
3	1, 2	ndnfrand-P7.4.RC 877	. . 3 ⊢ Ⅎ𝑥(∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑)
4		ndnfrex1-P7.8 833	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜓
5		rcp-NDASM2of3 196	. . . . . . 7 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑 ∧ (𝜑 → 𝜓)) → ∀𝑥𝜑)
6	5	alle-P7 941	. . . . . 6 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑 ∧ (𝜑 → 𝜓)) → 𝜑)
7		rcp-NDASM3of3 197	. . . . . 6 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑 ∧ (𝜑 → 𝜓)) → (𝜑 → 𝜓))
8	6, 7	ndime-P3.6 171	. . . . 5 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑 ∧ (𝜑 → 𝜓)) → 𝜓)
9	8	exi-P7 951	. . . 4 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑 ∧ (𝜑 → 𝜓)) → ∃𝑥𝜓)
10	9	rcp-NDIMI3 225	. . 3 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑) → ((𝜑 → 𝜓) → ∃𝑥𝜓))
11		rcp-NDASM1of2 193	. . 3 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑) → ∃𝑥(𝜑 → 𝜓))
12	3, 4, 10, 11	exe-P7 955	. 2 ⊢ ((∃𝑥(𝜑 → 𝜓) ∧ ∀𝑥𝜑) → ∃𝑥𝜓)
13	12	rcp-NDIMI2 224	1 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:  ∀wff-forall 8   → wff-imp 10   ∧ wff-and 132   ∧ wff-rcp-AND3 160  ∃wff-exists 595

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:  qimeqex-P7  1056  qimeqexint-P7  1057