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  7138  zdceq  9392  nn0lt2  9398  xlesubadd  9949  qdceq  10314  xrmaxadd  11404  nn0seqcvgd  12179  pcxnn0cl  12448  pcxqcl  12450  pcge0  12451  pcdvdsb  12458  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pc2dvds  12468  pcz  12470  pcprmpw2  12471  pcaddlem  12477  pcadd  12478  pcmpt  12481  qexpz  12490  4sqlem19  12547  lgsneg1  15141  lgsdirprm  15150  lgsdir  15151  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  2sqlem9  15211  tridceq  15546