Theorem neorian 3051

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

Assertion

Ref	Expression
neorian	⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))

Proof of Theorem neorian

Step	Hyp	Ref	Expression
1		df-ne 2957	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2957	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	orbi12i 925	. 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4		ianor 994	. 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
5	3, 4	bitr4i 280	1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ne 2957

This theorem is referenced by:  neneor  3056  poxp2  8118  oeoa  8562  recextlem2  11815  crne0  12185  crreczi  14238  gcdcllem3  16518  bezoutlem2  16557  nrhmzr  20566  dsmmacl  21773  mhpmulcl  22194  txhaus  23687  itg1addlem2  25739  coeaddlem  26289  dcubic  26888  creq0  32888  sibfof  34598  rrx2pnecoorneor  49301