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

Metamath Proof Explorer

Theorem cbv2h

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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbv2h.1 ⊢ φ → ψ → ∀ y ψ
2 cbv2h.2 ⊢ φ → χ → ∀ x χ
3 cbv2h.3 ⊢ φ → x = y → ψ ↔ χ
4 biimp ⊢ ψ ↔ χ → ψ → χ
5 3 4 syl6 ⊢ φ → x = y → ψ → χ
6 1 2 5 cbv1h ⊢ ∀ x ∀ y φ → ∀ x ψ → ∀ y χ
7 equcomi ⊢ y = x → x = y
8 biimpr ⊢ ψ ↔ χ → χ → ψ
9 7 3 8 syl56 ⊢ φ → y = x → χ → ψ
10 2 1 9 cbv1h ⊢ ∀ y ∀ x φ → ∀ y χ → ∀ x ψ
11 10 alcoms ⊢ ∀ x ∀ y φ → ∀ y χ → ∀ x ψ
12 6 11 impbid ⊢ ∀ x ∀ y φ → ∀ x ψ ↔ ∀ y χ