Theorem hbimdOLD 1816

Description: Obsolete proof of hbimd 1815 as of 16-Dec-2017. (Contributed by NM, 1-Jan-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

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

Proof of Theorem hbimdOLD

Step	Hyp	Ref	Expression
1		hbimd.1	. . . . 5 ⊢ (φ → ∀xφ)
2		hbimd.2	. . . . 5 ⊢ (φ → (ψ → ∀xψ))
3	1, 2	alrimih 1565	. . . 4 ⊢ (φ → ∀x(ψ → ∀xψ))
4		sp 1747	. . . . . 6 ⊢ (∀xψ → ψ)
5		hbn1 1730	. . . . . 6 ⊢ (¬ ∀xψ → ∀x ¬ ∀xψ)
6	4, 5	nsyl4 134	. . . . 5 ⊢ (¬ ∀x ¬ ∀xψ → ψ)
7	6	con1i 121	. . . 4 ⊢ (¬ ψ → ∀x ¬ ∀xψ)
8		con3 126	. . . . 5 ⊢ ((ψ → ∀xψ) → (¬ ∀xψ → ¬ ψ))
9	8	al2imi 1561	. . . 4 ⊢ (∀x(ψ → ∀xψ) → (∀x ¬ ∀xψ → ∀x ¬ ψ))
10	3, 7, 9	syl2im 34	. . 3 ⊢ (φ → (¬ ψ → ∀x ¬ ψ))
11		pm2.21 100	. . . 4 ⊢ (¬ ψ → (ψ → χ))
12	11	alimi 1559	. . 3 ⊢ (∀x ¬ ψ → ∀x(ψ → χ))
13	10, 12	syl6 29	. 2 ⊢ (φ → (¬ ψ → ∀x(ψ → χ)))
14		hbimd.3	. . 3 ⊢ (φ → (χ → ∀xχ))
15		ax-1 6	. . . 4 ⊢ (χ → (ψ → χ))
16	15	alimi 1559	. . 3 ⊢ (∀xχ → ∀x(ψ → χ))
17	14, 16	syl6 29	. 2 ⊢ (φ → (χ → ∀x(ψ → χ)))
18	13, 17	jad 154	1 ⊢ (φ → ((ψ → χ) → ∀x(ψ → χ)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This proof depends on definitions:  df-bi 177  df-ex 1542

This theorem is used by: (None)