Theorem neanior 3051

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1570   ≠ wne 2958

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 401  df-or 861  df-ne 2959

This theorem is referenced by:  nelpri  4621  nelprd  4623  eldifpr  4624  0nelop  5479  om00  8556  om00el  8557  oeoe  8581  mulne0b  11850  xmulpnf1  13295  lcmgcd  16660  lcmdvds  16661  domnmuln0  20808  isdomn3  20813  drngmulne0  20865  abvn0b  20939  lvecvsn0  21233  mdetralt  22765  ply1domn  26281  vieta1lem1  26471  vieta1lem2  26472  atandm  27041  atandm3  27043  dchrelbas3  27402  mulsne0bd  28379  eupth2lem3lem7  30585  frgrreg  30745  nmlno0lem  31145  nmlnop0iALT  32347  chirredi  32746  nelpr  32877  minplyirred  34101  subfacp1lem1  35671  filnetlem4  36892  disjecxrn  39061  lcvbr3  39797  cvrnbtwn4  40053  elpadd0  40583  cdleme0moN  40999  cdleme0nex  41064  mulltgt0d  43256  mullt0b2d  43258  sn-mullt0d  43259  fsuppind  43322  lidldomnnring  49001