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

Metamath Proof Explorer

Theorem sbievwOLD

Description: Obsolete version of sbievw as of 24-Aug-2025. (Contributed by NM, 30-Jun-1994) (Revised by BJ, 18-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sbievw.is ⊢ x = y → φ ↔ ψ
Assertion sbievwOLD ⊢ y x φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbievw.is ⊢ x = y → φ ↔ ψ
2 sb6 ⊢ y x φ ↔ ∀ x x = y → φ
3 1 equsalvw ⊢ ∀ x x = y → φ ↔ ψ
4 2 3 bitri ⊢ y x φ ↔ ψ