Theorem dvelimfALT2 1805

Description: Proof of dvelimf 2003 using dveeq2 1803 (shown as the last hypothesis) instead of ax12 1500. This shows that ax12 1500 could be replaced by dveeq2 1803 (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 1514	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
2		hbn1 1640	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
3		dvelimfALT2.4	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
4		dvelimfALT2.1	. . . . 5 ⊢ (𝜑 → ∀𝑥𝜑)
5	4	a1i 9	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
6	2, 3, 5	hbimd 1561	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ((𝑧 = 𝑦 → 𝜑) → ∀𝑥(𝑧 = 𝑦 → 𝜑)))
7	1, 6	hbald 1479	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑧(𝑧 = 𝑦 → 𝜑) → ∀𝑥∀𝑧(𝑧 = 𝑦 → 𝜑)))
8		dvelimfALT2.2	. . 3 ⊢ (𝜓 → ∀𝑧𝜓)
9		dvelimfALT2.3	. . 3 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
10	8, 9	equsalh 1714	. 2 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
11	10	albii 1458	. 2 ⊢ (∀𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ ∀𝑥𝜓)
12	7, 10, 11	3imtr3g 203	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104  ∀wal 1341   = wceq 1343

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-in1 604  ax-in2 605  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-fal 1349

This theorem is referenced by: (None)