Theorem sn-wcdeq 40169

Description: Alternative to wcdeq 3698 and df-cdeq 3699. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3699. (Contributed by SN, 26-Sep-2024.) (New usage is discouraged.)

Assertion

Ref	Expression
sn-wcdeq	wff (𝑥 = 𝑦 → 𝜑)

Proof of Theorem sn-wcdeq

Step	Hyp	Ref	Expression
1		wi 4	1 wff (𝑥 = 𝑦 → 𝜑)

Syntax hints:   → wi 4

This theorem is referenced by: (None)