Theorem neanior 3026

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 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2934	. . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷)
3	1, 2	anbi12i 629	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 991	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 275	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:  nelpri  4600  nelprd  4602  eldifpr  4603  0nelop  5445  om00  8504  om00el  8505  oeoe  8529  mulne0b  11785  xmulpnf1  13220  lcmgcd  16570  lcmdvds  16571  domnmuln0  20680  isdomn3  20686  drngmulne0  20733  abvn0b  20807  lvecvsn0  21102  mdetralt  22586  ply1domn  26102  vieta1lem1  26290  vieta1lem2  26291  atandm  26856  atandm3  26858  dchrelbas3  27218  mulsne0bd  28195  eupth2lem3lem7  30322  frgrreg  30482  nmlno0lem  30882  nmlnop0iALT  32084  chirredi  32483  nelpr  32619  minplyirred  33874  subfacp1lem1  35380  filnetlem4  36582  disjecxrn  38750  lcvbr3  39486  cvrnbtwn4  39742  elpadd0  40272  cdleme0moN  40688  cdleme0nex  40753  mulltgt0d  42944  mullt0b2d  42946  sn-mullt0d  42947  fsuppind  43040  lidldomnnring  48727