Theorem dral1 1728

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.)

Hypothesis

Ref	Expression
dral1.1	⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
dral1	⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))

Proof of Theorem dral1

Step	Hyp	Ref	Expression
1		hbae 1716	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑥∀𝑥 𝑥 = 𝑦)
2		dral1.1	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	biimpd 144	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → 𝜓))
4	1, 3	alimdh 1465	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑥𝜓))
5		ax10o 1713	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 → ∀𝑦𝜓))
6	4, 5	syld 45	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜓))
7		hbae 1716	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦∀𝑥 𝑥 = 𝑦)
8	2	biimprd 158	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜓 → 𝜑))
9	7, 8	alimdh 1465	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜓 → ∀𝑦𝜑))
10		ax10o 1713	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦𝜑 → ∀𝑥𝜑))
11	10	alequcoms 1514	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))
12	9, 11	syld 45	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜓 → ∀𝑥𝜑))
13	6, 12	impbid 129	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351

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-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  drnf1  1731  equveli  1757  a16g  1862