Theorem neanior 3063

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

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 385   ∨ wo 874   = wceq 1653   ≠ wne 2971

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 199  df-an 386  df-or 875  df-ne 2972

This theorem is referenced by:  nelpri  4393  nelprd  4395  eldifpr  4396  0nelop  5150  om00  7895  om00el  7896  oeoe  7919  mulne0b  10960  xmulpnf1  12353  lcmgcd  15655  lcmdvds  15656  drngmulne0  19087  lvecvsn0  19430  domnmuln0  19621  abvn0b  19625  mdetralt  20740  ply1domn  24224  vieta1lem1  24406  vieta1lem2  24407  atandm  24955  atandm3  24957  dchrelbas3  25315  eupth2lem3lem7  27579  frgrreg  27779  nmlno0lem  28173  nmlnop0iALT  29379  chirredi  29778  subfacp1lem1  31678  filnetlem4  32888  lcvbr3  35044  cvrnbtwn4  35300  elpadd0  35830  cdleme0moN  36246  cdleme0nex  36311  isdomn3  38567  lidldomnnring  42729