Theorem dcne 2386

Description: Decidable equality expressed in terms of ≠. Basically the same as df-dc 836. (Contributed by Jim Kingdon, 14-Mar-2020.)

Assertion

Ref	Expression
dcne	⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 836	. 2 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
2		df-ne 2376	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	orbi2i 763	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
4	1, 3	bitr4i 187	1 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1372   ≠ wne 2375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117  df-dc 836  df-ne 2376

This theorem is referenced by:  updjudhf  7163  zdceq  9430  nn0lt2  9436  xlesubadd  9987  qdceq  10368  xrmaxadd  11491  fsumdvds  12072  nn0seqcvgd  12282  pcxnn0cl  12552  pcxqcl  12554  pcge0  12555  pcdvdsb  12562  pcneg  12567  pcdvdstr  12569  pcgcd1  12570  pc2dvds  12572  pcz  12574  pcprmpw2  12575  pcaddlem  12581  pcadd  12582  pcmpt  12585  qexpz  12594  4sqlem19  12651  lgsneg1  15420  lgsdirprm  15429  lgsdir  15430  lgsne0  15433  lgsdirnn0  15442  lgsdinn0  15443  2sqlem9  15519  tridceq  15859