Theorem dcne 2378

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 2368	. . 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 2367

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 2368

This theorem is referenced by:  updjudhf  7154  zdceq  9418  nn0lt2  9424  xlesubadd  9975  qdceq  10351  xrmaxadd  11443  fsumdvds  12024  nn0seqcvgd  12234  pcxnn0cl  12504  pcxqcl  12506  pcge0  12507  pcdvdsb  12514  pcneg  12519  pcdvdstr  12521  pcgcd1  12522  pc2dvds  12524  pcz  12526  pcprmpw2  12527  pcaddlem  12533  pcadd  12534  pcmpt  12537  qexpz  12546  4sqlem19  12603  lgsneg1  15350  lgsdirprm  15359  lgsdir  15360  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  2sqlem9  15449  tridceq  15787