Theorem cbv1h 1978

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
cbv1h.1	⊢ (φ → (ψ → ∀yψ))
cbv1h.2	⊢ (φ → (χ → ∀xχ))
cbv1h.3	⊢ (φ → (x = y → (ψ → χ)))

Assertion

Ref	Expression
cbv1h	⊢ (∀x∀yφ → (∀xψ → ∀yχ))

Proof of Theorem cbv1h

Step	Hyp	Ref	Expression
1		cbv1h.1	. . . . 5 ⊢ (φ → (ψ → ∀yψ))
2	1	sps 1754	. . . 4 ⊢ (∀yφ → (ψ → ∀yψ))
3	2	al2imi 1561	. . 3 ⊢ (∀x∀yφ → (∀xψ → ∀x∀yψ))
4		ax-7 1734	. . 3 ⊢ (∀x∀yψ → ∀y∀xψ)
5	3, 4	syl6 29	. 2 ⊢ (∀x∀yφ → (∀xψ → ∀y∀xψ))
6		cbv1h.3	. . . . . . . 8 ⊢ (φ → (x = y → (ψ → χ)))
7	6	com23 72	. . . . . . 7 ⊢ (φ → (ψ → (x = y → χ)))
8		cbv1h.2	. . . . . . 7 ⊢ (φ → (χ → ∀xχ))
9	7, 8	syl6d 64	. . . . . 6 ⊢ (φ → (ψ → (x = y → ∀xχ)))
10	9	al2imi 1561	. . . . 5 ⊢ (∀xφ → (∀xψ → ∀x(x = y → ∀xχ)))
11		ax9o 1950	. . . . 5 ⊢ (∀x(x = y → ∀xχ) → χ)
12	10, 11	syl6 29	. . . 4 ⊢ (∀xφ → (∀xψ → χ))
13	12	al2imi 1561	. . 3 ⊢ (∀y∀xφ → (∀y∀xψ → ∀yχ))
14	13	a7s 1735	. 2 ⊢ (∀x∀yφ → (∀y∀xψ → ∀yχ))
15	5, 14	syld 40	1 ⊢ (∀x∀yφ → (∀xψ → ∀yχ))

This proof depends on syntax axioms:   → 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-7 1734  ax-11 1746  ax-12 1925

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is used by:  cbv1  1979  cbv2h  1980  cbv3h  1983