Theorem neanior 2915

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ≠ wne 2823

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 197  df-or 384  df-an 385  df-ne 2824

This theorem is referenced by:  nelpri  4234  nelprd  4236  eldifpr  4237  0nelop  4989  om00  7700  om00el  7701  oeoe  7724  mulne0b  10706  xmulpnf1  12142  lcmgcd  15367  lcmdvds  15368  drngmulne0  18817  lvecvsn0  19157  domnmuln0  19346  abvn0b  19350  mdetralt  20462  ply1domn  23928  vieta1lem1  24110  vieta1lem2  24111  atandm  24648  atandm3  24650  dchrelbas3  25008  eupth2lem3lem7  27212  frgrreg  27381  nmlno0lem  27776  nmlnop0iALT  28982  chirredi  29381  subfacp1lem1  31287  filnetlem4  32501  lcvbr3  34628  cvrnbtwn4  34884  elpadd0  35413  cdleme0moN  35830  cdleme0nex  35895  isdomn3  38099  lidldomnnring  42255