Theorem sn-wcdeq 43462

Description: Alternative to wcdeq 3728 and df-cdeq 3729. This flattens the syntax representation ( wi ( weq vx vy ) wph ) to ( sn-wcdeq vx vy wph ), illustrating the comment of df-cdeq 3729. (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 (𝑥 = 𝑦 → 𝜑)

This proof depends on syntax axioms:   → wi 4

This theorem is used by: (None)