Theorem hbimd 1566

Description: Deduction form of bound-variable hypothesis builder hbim 1538. (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 1503	. . . . 5 ⊢ (∀𝑥𝜓 → 𝜓)
4	3	imim1i 60	. . . 4 ⊢ ((𝜓 → ∀𝑥𝜒) → (∀𝑥𝜓 → ∀𝑥𝜒))
5		ax-i5r 1528	. . . 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 1460	. 2 ⊢ (𝜑 → (∀𝑥(∀𝑥𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
12	7, 11	syld 45	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))

Syntax hints:   → wi 4  ∀wal 1346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1440  ax-gen 1442  ax-4 1503  ax-i5r 1528

This theorem is referenced by:  hbbid  1568  19.21ht  1574  equveli  1752  dvelimfALT2  1810