Metamath Proof Explorer


Theorem neorian

Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007)

Ref Expression
Assertion neorian ( ( 𝐴𝐵𝐶𝐷 ) ↔ ¬ ( 𝐴 = 𝐵𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 df-ne ( 𝐴𝐵 ↔ ¬ 𝐴 = 𝐵 )
2 df-ne ( 𝐶𝐷 ↔ ¬ 𝐶 = 𝐷 )
3 1 2 orbi12i ( ( 𝐴𝐵𝐶𝐷 ) ↔ ( ¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷 ) )
4 ianor ( ¬ ( 𝐴 = 𝐵𝐶 = 𝐷 ) ↔ ( ¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷 ) )
5 3 4 bitr4i ( ( 𝐴𝐵𝐶𝐷 ) ↔ ¬ ( 𝐴 = 𝐵𝐶 = 𝐷 ) )