Theorem neanior 3018

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 2926	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2926	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	anbi12i 628	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 990	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 275	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ≠ wne 2925

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 848  df-ne 2926

This theorem is referenced by:  nelpri  4607  nelprd  4609  eldifpr  4610  0nelop  5439  om00  8493  om00el  8494  oeoe  8517  mulne0b  11761  xmulpnf1  13176  lcmgcd  16518  lcmdvds  16519  domnmuln0  20594  isdomn3  20600  drngmulne0  20647  abvn0b  20721  lvecvsn0  21016  mdetralt  22493  ply1domn  26027  vieta1lem1  26216  vieta1lem2  26217  atandm  26784  atandm3  26786  dchrelbas3  27147  mulsne0bd  28094  eupth2lem3lem7  30178  frgrreg  30338  nmlno0lem  30737  nmlnop0iALT  31939  chirredi  32338  nelpr  32475  minplyirred  33678  subfacp1lem1  35152  filnetlem4  36355  disjecxrn  38361  lcvbr3  39002  cvrnbtwn4  39258  elpadd0  39788  cdleme0moN  40204  cdleme0nex  40269  mulltgt0d  42455  mullt0b2d  42457  sn-mullt0d  42458  fsuppind  42563  lidldomnnring  48220