Theorem equsexd 1707

Description: Deduction form of equsex 1706. (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 117	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
5	4	imim2i 12	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜓 → 𝜒)))
6		pm3.31 260	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 → 𝜒)) → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
7	3, 5, 6	3syl 17	. . 3 ⊢ (𝜑 → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
8	1, 2, 7	exlimd2 1574	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
9		a9e 1674	. . . 4 ⊢ ∃𝑥 𝑥 = 𝑦
10	1	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → (𝜑 → ∀𝑥𝜑))
11	10, 2	jca 304	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)))
12		anim12 341	. . . . . . . 8 ⊢ (((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)) → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
13	11, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
14		19.26 1457	. . . . . . 7 ⊢ (∀𝑥(𝜑 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜒))
15	13, 14	syl6ibr 161	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒)))
16	15	anabsi5 568	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒))
17		idd 21	. . . . . . . 8 ⊢ (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦))
18	17	a1i 9	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦)))
19	18	imp 123	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
20		bi2 129	. . . . . . . . 9 ⊢ ((𝜓 ↔ 𝜒) → (𝜒 → 𝜓))
21	20	imim2i 12	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜒 → 𝜓)))
22		pm2.04 82	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜒 → 𝜓)) → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
23	3, 21, 22	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
24	23	imp 123	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝜓))
25	19, 24	jcad 305	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → (𝑥 = 𝑦 ∧ 𝜓)))
26	16, 25	eximdh 1590	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
27	9, 26	mpi 15	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
28	27	ex 114	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
29	8, 28	impbid 128	1 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1329   = wceq 1331  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cbvexdh  1896