Theorem neanior 3021

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 2929	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2929	. . 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 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  nelpri  4605  nelprd  4607  eldifpr  4608  0nelop  5434  om00  8490  om00el  8491  oeoe  8514  mulne0b  11758  xmulpnf1  13173  lcmgcd  16518  lcmdvds  16519  domnmuln0  20624  isdomn3  20630  drngmulne0  20677  abvn0b  20751  lvecvsn0  21046  mdetralt  22523  ply1domn  26056  vieta1lem1  26245  vieta1lem2  26246  atandm  26813  atandm3  26815  dchrelbas3  27176  mulsne0bd  28125  eupth2lem3lem7  30214  frgrreg  30374  nmlno0lem  30773  nmlnop0iALT  31975  chirredi  32374  nelpr  32511  minplyirred  33724  subfacp1lem1  35223  filnetlem4  36423  disjecxrn  38429  lcvbr3  39070  cvrnbtwn4  39326  elpadd0  39856  cdleme0moN  40272  cdleme0nex  40337  mulltgt0d  42523  mullt0b2d  42525  sn-mullt0d  42526  fsuppind  42631  lidldomnnring  48275