Theorem equsexd 1617

Description: Deduction form of equsex 1616. (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 111	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
5	4	imim2i 12	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜓 → 𝜒)))
6		pm3.31 249	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 → 𝜒)) → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
7	3, 5, 6	3syl 17	. . 3 ⊢ (𝜑 → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
8	1, 2, 7	exlimd2 1486	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
9		a9e 1586	. . . 4 ⊢ ∃𝑥 𝑥 = 𝑦
10	1	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → (𝜑 → ∀𝑥𝜑))
11	10, 2	jca 290	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)))
12		prth 326	. . . . . . . 8 ⊢ (((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)) → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
13	11, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
14		19.26 1370	. . . . . . 7 ⊢ (∀𝑥(𝜑 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜒))
15	13, 14	syl6ibr 151	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒)))
16	15	anabsi5 513	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒))
17		idd 21	. . . . . . . 8 ⊢ (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦))
18	17	a1i 9	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦)))
19	18	imp 115	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
20		bi2 121	. . . . . . . . 9 ⊢ ((𝜓 ↔ 𝜒) → (𝜒 → 𝜓))
21	20	imim2i 12	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜒 → 𝜓)))
22		pm2.04 76	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜒 → 𝜓)) → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
23	3, 21, 22	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
24	23	imp 115	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝜓))
25	19, 24	jcad 291	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → (𝑥 = 𝑦 ∧ 𝜓)))
26	16, 25	eximdh 1502	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
27	9, 26	mpi 15	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
28	27	ex 108	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
29	8, 28	impbid 120	1 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241   = wceq 1243  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  cbvexdh  1801