Theorem dcne 2371

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 2361	. . 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 1364   ≠ wne 2360

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 2361

This theorem is referenced by:  updjudhf  7109  zdceq  9359  nn0lt2  9365  xlesubadd  9915  qdceq  10279  xrmaxadd  11304  nn0seqcvgd  12076  pcxnn0cl  12345  pcxqcl  12347  pcge0  12348  pcdvdsb  12355  pcneg  12360  pcdvdstr  12362  pcgcd1  12363  pc2dvds  12365  pcz  12367  pcprmpw2  12368  pcaddlem  12374  pcadd  12375  pcmpt  12378  qexpz  12387  4sqlem19  12444  lgsneg1  14904  lgsdirprm  14913  lgsdir  14914  lgsne0  14917  lgsdirnn0  14926  lgsdinn0  14927  2sqlem9  14949  tridceq  15283