Theorem neanior 3029

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 397   ∨ wo 854   = wceq 1548   ≠ wne 2936

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 209  df-an 398  df-or 855  df-ne 2937

This theorem is referenced by:  nelpri  4590  nelprd  4592  eldifpr  4593  0nelop  5440  om00  8504  om00el  8505  oeoe  8529  mulne0b  11786  xmulpnf1  13221  lcmgcd  16571  lcmdvds  16572  domnmuln0  20685  isdomn3  20691  drngmulne0  20738  abvn0b  20812  lvecvsn0  21106  mdetralt  22595  ply1domn  26111  vieta1lem1  26298  vieta1lem2  26299  atandm  26862  atandm3  26864  dchrelbas3  27223  mulsne0bd  28200  eupth2lem3lem7  30326  frgrreg  30486  nmlno0lem  30886  nmlnop0iALT  32088  chirredi  32487  nelpr  32623  minplyirred  33907  subfacp1lem1  35422  filnetlem4  36624  disjecxrn  38794  lcvbr3  39530  cvrnbtwn4  39786  elpadd0  40316  cdleme0moN  40732  cdleme0nex  40797  mulltgt0d  42987  mullt0b2d  42989  sn-mullt0d  42990  fsuppind  43055  lidldomnnring  48741