Metamath Proof Explorer

Theorem sb4OLD

Description: Obsolete as of 30-Jul-2023. Use sb4b instead. One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993) Revise df-sb . (Revised by Wolf Lammen, 25-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sb4OLD ¬ x x = y y x φ x x = y φ


Step Hyp Ref Expression
1 sb4b ¬ x x = y y x φ x x = y φ
2 1 biimpd ¬ x x = y y x φ x x = y φ