Theorem hbimd 1109

Description: Deduction form of bound-variable hypothesis builder hbim 1006.

Hypotheses

Ref	Expression
hbimd.1	⊢ (φ → ∀xφ)
hbimd.2	⊢ (φ → (ψ → ∀xψ))
hbimd.3	⊢ (φ → (χ → ∀xχ))

Assertion

Ref	Expression
hbimd	⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))

Proof of Theorem hbimd

Step	Hyp	Ref	Expression
1		hbimd.1	. . . . 5 ⊢ (φ → ∀xφ)
2		hbimd.2	. . . . 5 ⊢ (φ → (ψ → ∀xψ))
3	1, 2	hbnd 1108	. . . 4 ⊢ (φ → (¬ ψ → ∀x ¬ ψ))
4		pm2.21 76	. . . . 5 ⊢ (¬ ψ → (ψ → χ))
5	4	19.20i 991	. . . 4 ⊢ (∀x ¬ ψ → ∀x(ψ → χ))
6	3, 5	syl6com 53	. . 3 ⊢ (¬ ψ → (φ → ∀x(ψ → χ)))
7		hbimd.3	. . . 4 ⊢ (φ → (χ → ∀xχ))
8		ax-1 4	. . . . 5 ⊢ (χ → (ψ → χ))
9	8	19.20i 991	. . . 4 ⊢ (∀xχ → ∀x(ψ → χ))
10	7, 9	syl6com 53	. . 3 ⊢ (χ → (φ → ∀x(ψ → χ)))
11	6, 10	ja 137	. 2 ⊢ ((ψ → χ) → (φ → ∀x(ψ → χ)))
12	11	com12 11	1 ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 953

This theorem is referenced by:  hbbid 1111  19.21t 1114  dvelimfALT 1152  hbsb4 1247  dvelimALT 1352  a12lem1 1375  ralcom2 1774  reuuni2f 2879  axrepndlem1 4927  axrepndlem2 4928  axunndlem1 4930  axunnd 4931  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregndlem2 4938  axregnd 4939  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-6o 977

Copyright terms: Public domain