Theorem hbimd 1465

Description: Deduction form of bound-variable hypothesis builder hbim 1437. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.)

Hypotheses

Ref	Expression
hbimd.1	⊢ (𝜑 → ∀𝑥𝜑)
hbimd.2	⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
hbimd.3	⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))

Assertion

Ref	Expression
hbimd	⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))

Proof of Theorem hbimd

Step	Hyp	Ref	Expression
1		hbimd.3	. . . 4 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))
2	1	imim2d 48	. . 3 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → ∀𝑥𝜒)))
3		ax-4 1400	. . . . 5 ⊢ (∀𝑥𝜓 → 𝜓)
4	3	imim1i 54	. . . 4 ⊢ ((𝜓 → ∀𝑥𝜒) → (∀𝑥𝜓 → ∀𝑥𝜒))
5		ax-i5r 1428	. . . 4 ⊢ ((∀𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒))
6	4, 5	syl 14	. . 3 ⊢ ((𝜓 → ∀𝑥𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒))
7	2, 6	syl6 29	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒)))
8		hbimd.1	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
9		hbimd.2	. . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
10	9	imim1d 69	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → 𝜒) → (𝜓 → 𝜒)))
11	8, 10	alimdh 1356	. 2 ⊢ (𝜑 → (∀𝑥(∀𝑥𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
12	7, 11	syld 40	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))

Syntax hints:   → wi 4  ∀wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1336  ax-gen 1338  ax-4 1400  ax-i5r 1428

This theorem is referenced by:  hbbid  1467  19.21ht  1473  equveli  1642  dvelimfALT2  1698