Theorem neanior 3027

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 846   = wceq 1542   ≠ wne 2935

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 210  df-an 400  df-or 847  df-ne 2936

This theorem is referenced by:  nelpri  4555  nelprd  4557  eldifpr  4558  0nelop  5363  om00  8244  om00el  8245  oeoe  8268  mulne0b  11371  xmulpnf1  12762  lcmgcd  16060  lcmdvds  16061  drngmulne0  19655  lvecvsn0  20012  domnmuln0  20202  abvn0b  20206  mdetralt  21371  ply1domn  24888  vieta1lem1  25070  vieta1lem2  25071  atandm  25626  atandm3  25628  dchrelbas3  25986  eupth2lem3lem7  28183  frgrreg  28343  nmlno0lem  28740  nmlnop0iALT  29942  chirredi  30341  nelpr  30465  subfacp1lem1  32724  filnetlem4  34225  lcvbr3  36692  cvrnbtwn4  36948  elpadd0  37478  cdleme0moN  37894  cdleme0nex  37959  fsuppind  39898  isdomn3  40641  lidldomnnring  45069