Theorem neanior 3025

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 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2933	. . 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 2932

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 2933

This theorem is referenced by:  nelpri  4631  nelprd  4633  eldifpr  4634  0nelop  5471  om00  8587  om00el  8588  oeoe  8611  mulne0b  11878  xmulpnf1  13290  lcmgcd  16626  lcmdvds  16627  domnmuln0  20669  isdomn3  20675  drngmulne0  20722  abvn0b  20796  lvecvsn0  21070  mdetralt  22546  ply1domn  26081  vieta1lem1  26270  vieta1lem2  26271  atandm  26838  atandm3  26840  dchrelbas3  27201  mulsne0bd  28141  eupth2lem3lem7  30215  frgrreg  30375  nmlno0lem  30774  nmlnop0iALT  31976  chirredi  32375  nelpr  32512  minplyirred  33745  subfacp1lem1  35201  filnetlem4  36399  disjecxrn  38407  lcvbr3  39041  cvrnbtwn4  39297  elpadd0  39828  cdleme0moN  40244  cdleme0nex  40309  fsuppind  42613  lidldomnnring  48211