Theorem dcne 2375

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 2365	. . 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 2364

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 2365

This theorem is referenced by:  updjudhf  7140  zdceq  9395  nn0lt2  9401  xlesubadd  9952  qdceq  10317  xrmaxadd  11407  nn0seqcvgd  12182  pcxnn0cl  12451  pcxqcl  12453  pcge0  12454  pcdvdsb  12461  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcz  12473  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  pcmpt  12484  qexpz  12493  4sqlem19  12550  lgsneg1  15182  lgsdirprm  15191  lgsdir  15192  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  2sqlem9  15281  tridceq  15616