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  4614  nelprd  4616  eldifpr  4617  0nelop  5452  om00  8512  om00el  8513  oeoe  8537  mulne0b  11790  xmulpnf1  13201  lcmgcd  16546  lcmdvds  16547  domnmuln0  20654  isdomn3  20660  drngmulne0  20707  abvn0b  20781  lvecvsn0  21076  mdetralt  22564  ply1domn  26097  vieta1lem1  26286  vieta1lem2  26287  atandm  26854  atandm3  26856  dchrelbas3  27217  mulsne0bd  28194  eupth2lem3lem7  30321  frgrreg  30481  nmlno0lem  30881  nmlnop0iALT  32083  chirredi  32482  nelpr  32618  minplyirred  33889  subfacp1lem1  35395  filnetlem4  36597  disjecxrn  38663  lcvbr3  39399  cvrnbtwn4  39655  elpadd0  40185  cdleme0moN  40601  cdleme0nex  40666  mulltgt0d  42852  mullt0b2d  42854  sn-mullt0d  42855  fsuppind  42948  lidldomnnring  48596