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 627	. 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷))
4		pm4.56 987	. 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))
5	3, 4	bitri 274	1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷))

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ≠ 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 206  df-an 397  df-or 846  df-ne 2941

This theorem is referenced by:  nelpri  4656  nelprd  4658  eldifpr  4659  0nelop  5495  om00  8571  om00el  8572  oeoe  8595  mulne0b  11851  xmulpnf1  13249  lcmgcd  16540  lcmdvds  16541  drngmulne0  20337  lvecvsn0  20714  domnmuln0  20906  abvn0b  20912  mdetralt  22101  ply1domn  25632  vieta1lem1  25814  vieta1lem2  25815  atandm  26370  atandm3  26372  dchrelbas3  26730  eupth2lem3lem7  29476  frgrreg  29636  nmlno0lem  30033  nmlnop0iALT  31235  chirredi  31634  nelpr  31755  minplyirred  32758  subfacp1lem1  34158  filnetlem4  35254  disjecxrn  37247  lcvbr3  37881  cvrnbtwn4  38137  elpadd0  38668  cdleme0moN  39084  cdleme0nex  39149  fsuppind  41159  isdomn3  41931  lidldomnnring  46781