Theorem dvelimfALT2 1865

Description: Proof of dvelimf 2068 using dveeq2 1863 (shown as the last hypothesis) instead of ax12 1561. This shows that ax12 1561 could be replaced by dveeq2 1863 (the last hypothesis). (Contributed by Andrew Salmon, 21-Jul-2011.)

Hypotheses

Ref	Expression
dvelimfALT2.1	⊢ (𝜑 → ∀𝑥𝜑)
dvelimfALT2.2	⊢ (𝜓 → ∀𝑧𝜓)
dvelimfALT2.3	⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
dvelimfALT2.4	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))

Assertion

Ref	Expression
dvelimfALT2	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)

Proof of Theorem dvelimfALT2

Step	Hyp	Ref	Expression
1		ax-17 1575	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
2		hbn1 1700	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
3		dvelimfALT2.4	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4		dvelimfALT2.1	. . . . 5 ⊢ (𝜑 → ∀𝑥𝜑)
5	4	a1i 9	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
6	2, 3, 5	hbimd 1622	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ((𝑧 = 𝑦 → 𝜑) → ∀𝑥(𝑧 = 𝑦 → 𝜑)))
7	1, 6	hbald 1540	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑦 → 𝜑) → ∀𝑥∀𝑧(𝑧 = 𝑦 → 𝜑)))
8		dvelimfALT2.2	. . 3 ⊢ (𝜓 → ∀𝑧𝜓)
9		dvelimfALT2.3	. . 3 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
10	8, 9	equsalh 1774	. 2 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
11	10	albii 1519	. 2 ⊢ (∀𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ ∀𝑥𝜓)
12	7, 10, 11	3imtr3g 204	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398

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-in1 619  ax-in2 620  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404

This theorem is referenced by: (None)