Theorem equsexd 1743

Description: Deduction form of equsex 1742. (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		biimp 118	. . . . 5 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
5	4	imim2i 12	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜓 → 𝜒)))
6		pm3.31 262	. . . 4 ⊢ ((𝑥 = 𝑦 → (𝜓 → 𝜒)) → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
7	3, 5, 6	3syl 17	. . 3 ⊢ (𝜑 → ((𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
8	1, 2, 7	exlimd2 1609	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) → 𝜒))
9		a9e 1710	. . . 4 ⊢ ∃𝑥 𝑥 = 𝑦
10	1	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → (𝜑 → ∀𝑥𝜑))
11	10, 2	jca 306	. . . . . . . 8 ⊢ (𝜑 → ((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)))
12		anim12 344	. . . . . . . 8 ⊢ (((𝜑 → ∀𝑥𝜑) ∧ (𝜒 → ∀𝑥𝜒)) → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
13	11, 12	syl 14	. . . . . . 7 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → (∀𝑥𝜑 ∧ ∀𝑥𝜒)))
14		19.26 1495	. . . . . . 7 ⊢ (∀𝑥(𝜑 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜒))
15	13, 14	imbitrrdi 162	. . . . . 6 ⊢ (𝜑 → ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒)))
16	15	anabsi5 579	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜒))
17		idd 21	. . . . . . . 8 ⊢ (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦))
18	17	a1i 9	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝑥 = 𝑦)))
19	18	imp 124	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝑥 = 𝑦))
20		biimpr 130	. . . . . . . . 9 ⊢ ((𝜓 ↔ 𝜒) → (𝜒 → 𝜓))
21	20	imim2i 12	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) → (𝑥 = 𝑦 → (𝜒 → 𝜓)))
22		pm2.04 82	. . . . . . . 8 ⊢ ((𝑥 = 𝑦 → (𝜒 → 𝜓)) → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
23	3, 21, 22	3syl 17	. . . . . . 7 ⊢ (𝜑 → (𝜒 → (𝑥 = 𝑦 → 𝜓)))
24	23	imp 124	. . . . . 6 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → 𝜓))
25	19, 24	jcad 307	. . . . 5 ⊢ ((𝜑 ∧ 𝜒) → (𝑥 = 𝑦 → (𝑥 = 𝑦 ∧ 𝜓)))
26	16, 25	eximdh 1625	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → (∃𝑥 𝑥 = 𝑦 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
27	9, 26	mpi 15	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))
28	27	ex 115	. 2 ⊢ (𝜑 → (𝜒 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜓)))
29	8, 28	impbid 129	1 ⊢ (𝜑 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜓) ↔ 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362   = wceq 1364  ∃wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cbvexdh  1941