Theorem hbimd 1552

Description: Deduction form of bound-variable hypothesis builder hbim 1524. (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 54	. . 3 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → ∀𝑥𝜒)))
3		ax-4 1487	. . . . 5 ⊢ (∀𝑥𝜓 → 𝜓)
4	3	imim1i 60	. . . 4 ⊢ ((𝜓 → ∀𝑥𝜒) → (∀𝑥𝜓 → ∀𝑥𝜒))
5		ax-i5r 1515	. . . 4 ⊢ ((∀𝑥𝜓 → ∀𝑥𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒))
6	4, 5	syl 14	. . 3 ⊢ ((𝜓 → ∀𝑥𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒))
7	2, 6	syl6 33	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(∀𝑥𝜓 → 𝜒)))
8		hbimd.1	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
9		hbimd.2	. . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
10	9	imim1d 75	. . 3 ⊢ (𝜑 → ((∀𝑥𝜓 → 𝜒) → (𝜓 → 𝜒)))
11	8, 10	alimdh 1443	. 2 ⊢ (𝜑 → (∀𝑥(∀𝑥𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
12	7, 11	syld 45	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))

Syntax hints:   → wi 4  ∀wal 1329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1423  ax-gen 1425  ax-4 1487  ax-i5r 1515

This theorem is referenced by:  hbbid  1554  19.21ht  1560  equveli  1732  dvelimfALT2  1789