Theorem neorian 3028

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 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2934	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	orbi12i 915	. 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
4		ianor 984	. 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷))
5	3, 4	bitr4i 278	1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ≠ wne 2933

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 207  df-an 396  df-or 849  df-ne 2934

This theorem is referenced by:  neneor  3033  poxp2  8095  oeoa  8535  recextlem2  11780  crne0  12150  crreczi  14163  gcdcllem3  16440  bezoutlem2  16479  nrhmzr  20482  dsmmacl  21708  mhpmulcl  22104  txhaus  23603  itg1addlem2  25666  coeaddlem  26222  dcubic  26824  creq0  32825  sibfof  34517  rrx2pnecoorneor  49069