Theorem neanior 3050

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1560   ≠ wne 2957

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 400  df-or 859  df-ne 2958

This theorem is referenced by:  nelpri  4614  nelprd  4616  eldifpr  4617  0nelop  5465  om00  8544  om00el  8545  oeoe  8569  mulne0b  11828  xmulpnf1  13277  lcmgcd  16641  lcmdvds  16642  domnmuln0  20755  isdomn3  20761  drngmulne0  20808  abvn0b  20882  lvecvsn0  21176  mdetralt  22665  ply1domn  26181  vieta1lem1  26371  vieta1lem2  26372  atandm  26938  atandm3  26940  dchrelbas3  27299  mulsne0bd  28276  eupth2lem3lem7  30433  frgrreg  30593  nmlno0lem  30993  nmlnop0iALT  32195  chirredi  32594  nelpr  32727  minplyirred  34005  subfacp1lem1  35526  filnetlem4  36738  disjecxrn  38908  lcvbr3  39644  cvrnbtwn4  39900  elpadd0  40430  cdleme0moN  40846  cdleme0nex  40911  mulltgt0d  43101  mullt0b2d  43103  sn-mullt0d  43104  fsuppind  43169  lidldomnnring  48855