Theorem neanior 2874

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

Assertion

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

Proof of Theorem neanior

Step	Hyp	Ref	Expression
1		df-ne 2782	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2782	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	anbi12i 729	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 515	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 263	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ≠ wne 2780

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 196  df-or 384  df-an 385  df-ne 2782

This theorem is referenced by:  nelpri  4149  nelprd  4151  eldifpr  4152  0nelop  4886  om00  7542  om00el  7543  oeoe  7566  mulne0b  10547  xmulpnf1  11976  lcmgcd  15158  lcmdvds  15159  drngmulne0  18592  lvecvsn0  18930  domnmuln0  19119  abvn0b  19123  mdetralt  20233  ply1domn  23687  vieta1lem1  23869  vieta1lem2  23870  atandm  24403  atandm3  24405  dchrelbas3  24763  vdgr1a  26433  nmlno0lem  27032  nmlnop0iALT  28238  chirredi  28637  subfacp1lem1  30415  filnetlem4  31546  lcvbr3  33328  cvrnbtwn4  33584  elpadd0  34113  cdleme0moN  34530  cdleme0nex  34595  isdomn3  36801  eupth2lem3lem7  41402  av-frgrareg  41548  lidldomnnring  41720