Theorem hbim1 1459

Description: A closed form of hbim 1434. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem hbim1

Step	Hyp	Ref	Expression
1		hbim1.2	. . 3 ⊢ (φ → (ψ → ∀xψ))
2	1	a2i 11	. 2 ⊢ ((φ → ψ) → (φ → ∀xψ))
3		hbim1.1	. . 3 ⊢ (φ → ∀xφ)
4	3	19.21h 1446	. 2 ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
5	2, 4	sylibr 137	1 ⊢ ((φ → ψ) → ∀x(φ → ψ))

Syntax hints:   → wi 4  ∀wal 1240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfim1  1460  sbco2d  1837  sbco2vd  1838