This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbv1h

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 13-May-2018) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbv1h.1 ⊢ φ → ψ → ∀ y ψ
2 cbv1h.2 ⊢ φ → χ → ∀ x χ
3 cbv1h.3 ⊢ φ → x = y → ψ → χ
4 nfa1 ⊢ Ⅎ x ∀ x ∀ y φ
5 nfa2 ⊢ Ⅎ y ∀ x ∀ y φ
6 2sp ⊢ ∀ x ∀ y φ → φ
7 6 1 syl ⊢ ∀ x ∀ y φ → ψ → ∀ y ψ
8 5 7 nf5d ⊢ ∀ x ∀ y φ → Ⅎ y ψ
9 6 2 syl ⊢ ∀ x ∀ y φ → χ → ∀ x χ
10 4 9 nf5d ⊢ ∀ x ∀ y φ → Ⅎ x χ
11 6 3 syl ⊢ ∀ x ∀ y φ → x = y → ψ → χ
12 4 5 8 10 11 cbv1 ⊢ ∀ x ∀ y φ → ∀ x ψ → ∀ y χ