Theorem hbim 702

Description: If x is not free in φ and ψ, it is not free in (φ → ψ).

Hypotheses

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

Assertion

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

Proof of Theorem hbim

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 ⊢ (φ → ∀xφ)
2	1	hbne 699	. . 3 ⊢ (¬ φ → ∀x ¬ φ)
3		pm2.21 71	. . . 4 ⊢ (¬ φ → (φ → ψ))
4	3	19.20i 691	. . 3 ⊢ (∀x ¬ φ → ∀x(φ → ψ))
5	2, 4	syl 12	. 2 ⊢ (¬ φ → ∀x(φ → ψ))
6		hb.2	. . 3 ⊢ (ψ → ∀xψ)
7		ax-1 3	. . . 4 ⊢ (ψ → (φ → ψ))
8	7	19.20i 691	. . 3 ⊢ (∀xψ → ∀x(φ → ψ))
9	6, 8	syl 12	. 2 ⊢ (ψ → ∀x(φ → ψ))
10	5, 9	ja 118	1 ⊢ ((φ → ψ) → ∀x(φ → ψ))

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672

This theorem is referenced by:  hbor 703  hban 704  hbbi 705  19.21 738  19.23 745  19.38 760  mo 1020  hbmo1 1032  hbmo 1033  moexex 1058  2eu4 1070  hbral 1236  cbvralf 1330  vtocl2gf 1385  axrep2 1474  dfss2f 1499  reuuni2 1956  hbint 1975  elintab 1976  ssiun2s 2020  opabsb 2114  tfis 2245  onminex 2275  findes 2400  tfinds 2401  tfindes 2404  ralxp 2456  dmcosseq 2572  fneu 2728  fv3 2839  tz6.12c 2846  fvopab2 2878  f1fvf 2917  tfr3 2964  dom2d 3307  aceq1 3552  aceq5lem5 3562  zfcndrep 3760  zfcndinf 3764  suppsrlem 4015  suppsr3 4018  uzind 4603  nnwof 4609  nn0ind 4612  chcmh 5148  atom1d 5750

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

metamath.org