Theorem neanior 3041

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ≠ wne 2946

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 847  df-ne 2947

This theorem is referenced by:  nelpri  4677  nelprd  4679  eldifpr  4680  0nelop  5515  om00  8631  om00el  8632  oeoe  8655  mulne0b  11931  xmulpnf1  13336  lcmgcd  16654  lcmdvds  16655  domnmuln0  20731  isdomn3  20737  drngmulne0  20784  abvn0b  20859  lvecvsn0  21134  mdetralt  22635  ply1domn  26183  vieta1lem1  26370  vieta1lem2  26371  atandm  26937  atandm3  26939  dchrelbas3  27300  mulsne0bd  28230  eupth2lem3lem7  30266  frgrreg  30426  nmlno0lem  30825  nmlnop0iALT  32027  chirredi  32426  nelpr  32559  minplyirred  33704  subfacp1lem1  35147  filnetlem4  36347  disjecxrn  38345  lcvbr3  38979  cvrnbtwn4  39235  elpadd0  39766  cdleme0moN  40182  cdleme0nex  40247  fsuppind  42545  lidldomnnring  47959