Metamath Proof Explorer


Theorem neor

Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007)

Ref Expression
Assertion neor ( ( 𝐴 = 𝐵𝜓 ) ↔ ( 𝐴𝐵𝜓 ) )

Proof

Step Hyp Ref Expression
1 df-or ( ( 𝐴 = 𝐵𝜓 ) ↔ ( ¬ 𝐴 = 𝐵𝜓 ) )
2 df-ne ( 𝐴𝐵 ↔ ¬ 𝐴 = 𝐵 )
3 2 imbi1i ( ( 𝐴𝐵𝜓 ) ↔ ( ¬ 𝐴 = 𝐵𝜓 ) )
4 1 3 bitr4i ( ( 𝐴 = 𝐵𝜓 ) ↔ ( 𝐴𝐵𝜓 ) )