Theorem equsexd 1657

Description: Deduction form of equsex 1656. (Contributed by Jim Kingdon, 29-Dec-2017.)

Hypotheses

Ref	Expression
equsexd.1	⊢ (𝜑 → ∀𝑥𝜑)
equsexd.2	⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))
equsexd.3	⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))

Assertion

Ref	Expression
equsexd	⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))

Proof of Theorem equsexd

Step	Hyp	Ref	Expression
1		equsexd.1	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
2		equsexd.2	. . 3 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))
3		equsexd.3	. . . 4 ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))
4		bi1 116	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
5	4	imim2i 12	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜓 → 𝜒)))
6		pm3.31 258	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 → 𝜒)) → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
7	3, 5, 6	3syl 17	. . 3 ⊢ (𝜑 → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
8	1, 2, 7	exlimd2 1526	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
9		a9e 1626	. . . 4 ⊢ ∃𝑥 𝑥 = 𝑦
10	1	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → (𝜑 → ∀𝑥𝜑))
11	10, 2	jca 300	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)))
12		prth 336	. . . . . . . 8 ⊢ (((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)) → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
13	11, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
14		19.26 1410	. . . . . . 7 ⊢ (∀𝑥(𝜑 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜒))
15	13, 14	syl6ibr 160	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒)))
16	15	anabsi5 543	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒))
17		idd 21	. . . . . . . 8 ⊢ (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦))
18	17	a1i 9	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦)))
19	18	imp 122	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
20		bi2 128	. . . . . . . . 9 ⊢ ((𝜓 ↔ 𝜒) → (𝜒 → 𝜓))
21	20	imim2i 12	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜒 → 𝜓)))
22		pm2.04 81	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜒 → 𝜓)) → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
23	3, 21, 22	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
24	23	imp 122	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝜓))
25	19, 24	jcad 301	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → (𝑥 = 𝑦 ∧ 𝜓)))
26	16, 25	eximdh 1542	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
27	9, 26	mpi 15	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
28	27	ex 113	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
29	8, 28	impbid 127	1 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103  ∀wal 1282   = wceq 1284  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  cbvexdh  1842