Theorem cbvald 977

Description: Deduction used to change bound variables with implicit substitution, particularly useful in conjunction with ddelim 1000.

Hypotheses

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

Assertion

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

Distinct variable group(s):   φ,x   χ,x

Proof of Theorem cbvald

Step	Hyp	Ref	Expression
1		cbvald.1	. . . . 5 ⊢ (φ → ∀yφ)
2		cbvald.2	. . . . 5 ⊢ (φ → (ψ → ∀yψ))
3	1, 2	hbim1 781	. . . 4 ⊢ ((φ → ψ) → ∀y(φ → ψ))
4		ax-17 925	. . . 4 ⊢ ((φ → χ) → ∀x(φ → χ))
5		cbvald.3	. . . . . 6 ⊢ (φ → (x = y → (ψ ↔ χ)))
6	5	com12 13	. . . . 5 ⊢ (x = y → (φ → (ψ ↔ χ)))
7	6	pm5.74d 444	. . . 4 ⊢ (x = y → ((φ → ψ) ↔ (φ → χ)))
8	3, 4, 7	cbval 848	. . 3 ⊢ (∀x(φ → ψ) ↔ ∀y(φ → χ))
9		19.21v 942	. . 3 ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
10	1	19.21 738	. . 3 ⊢ (∀y(φ → χ) ↔ (φ → ∀yχ))
11	8, 9, 10	3bitr3 156	. 2 ⊢ ((φ → ∀xψ) ↔ (φ → ∀yχ))
12	11	pm5.74ri 445	1 ⊢ (φ → (∀xψ ↔ ∀yχ))

Syntax hints:   → wi 2   ↔ wb 127  ∀wal 672   = weq 797

This theorem is referenced by:  cbvexd 978  axextnd 3737  axrepndlem1 3738  axunndlem1 3741  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

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-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org