Theorem hbimOLD 1818

Description: Obsolete proof of hbim 1817 as of 1-Jan-2018. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
hbim.1	⊢ (φ → ∀xφ)
hbim.2	⊢ (ψ → ∀xψ)

Assertion

Ref	Expression
hbimOLD	⊢ ((φ → ψ) → ∀x(φ → ψ))

Proof of Theorem hbimOLD

Step	Hyp	Ref	Expression
1		hbim.1	. . . 4 ⊢ (φ → ∀xφ)
2	1	hbn 1776	. . 3 ⊢ (¬ φ → ∀x ¬ φ)
3		pm2.21 100	. . 3 ⊢ (¬ φ → (φ → ψ))
4	2, 3	alrimih 1565	. 2 ⊢ (¬ φ → ∀x(φ → ψ))
5		hbim.2	. . 3 ⊢ (ψ → ∀xψ)
6		ax-1 6	. . 3 ⊢ (ψ → (φ → ψ))
7	5, 6	alrimih 1565	. 2 ⊢ (ψ → ∀x(φ → ψ))
8	4, 7	ja 153	1 ⊢ ((φ → ψ) → ∀x(φ → ψ))

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540

This theorem was proved from 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 theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by: (None)