Theorem neanior 3035

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  nelpri  4655  nelprd  4657  eldifpr  4658  0nelop  5501  om00  8613  om00el  8614  oeoe  8637  mulne0b  11904  xmulpnf1  13316  lcmgcd  16644  lcmdvds  16645  domnmuln0  20709  isdomn3  20715  drngmulne0  20762  abvn0b  20837  lvecvsn0  21111  mdetralt  22614  ply1domn  26163  vieta1lem1  26352  vieta1lem2  26353  atandm  26919  atandm3  26921  dchrelbas3  27282  mulsne0bd  28212  eupth2lem3lem7  30253  frgrreg  30413  nmlno0lem  30812  nmlnop0iALT  32014  chirredi  32413  nelpr  32549  minplyirred  33754  subfacp1lem1  35184  filnetlem4  36382  disjecxrn  38390  lcvbr3  39024  cvrnbtwn4  39280  elpadd0  39811  cdleme0moN  40227  cdleme0nex  40292  fsuppind  42600  lidldomnnring  48152