Theorem neanior 3025

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 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		df-ne 2933	. . 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 2932

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 2933

This theorem is referenced by:  nelpri  4599  nelprd  4601  eldifpr  4602  0nelop  5450  om00  8510  om00el  8511  oeoe  8535  mulne0b  11791  xmulpnf1  13226  lcmgcd  16576  lcmdvds  16577  domnmuln0  20686  isdomn3  20692  drngmulne0  20739  abvn0b  20813  lvecvsn0  21107  mdetralt  22573  ply1domn  26089  vieta1lem1  26276  vieta1lem2  26277  atandm  26840  atandm3  26842  dchrelbas3  27201  mulsne0bd  28178  eupth2lem3lem7  30304  frgrreg  30464  nmlno0lem  30864  nmlnop0iALT  32066  chirredi  32465  nelpr  32601  minplyirred  33855  subfacp1lem1  35361  filnetlem4  36563  disjecxrn  38733  lcvbr3  39469  cvrnbtwn4  39725  elpadd0  40255  cdleme0moN  40671  cdleme0nex  40736  mulltgt0d  42927  mullt0b2d  42929  sn-mullt0d  42930  fsuppind  43023  lidldomnnring  48712