Theorem dcne 2423

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 716  DECID wdc 842   = wceq 1398   ≠ wne 2412

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 717

This theorem depends on definitions:  df-bi 117  df-dc 843  df-ne 2413

This theorem is referenced by:  updjudhf  7370  pr1or2  7491  zdceq  9653  nn0lt2  9659  xlesubadd  10216  qdceq  10604  ccat1st1st  11329  swrdccatin1  11417  xrmaxadd  11946  fsumdvds  12528  nn0seqcvgd  12738  pcxnn0cl  13008  pcxqcl  13010  pcge0  13011  pcdvdsb  13018  pcneg  13023  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcz  13030  pcprmpw2  13031  pcaddlem  13037  pcadd  13038  pcmpt  13041  qexpz  13050  4sqlem19  13107  lgsneg1  15898  lgsdirprm  15907  lgsdir  15908  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  2sqlem9  15997  upgr1een  16119  usgr1e  16236  eupth2lem3lem3fi  16465  eupth2lem3lem7fi  16469  tridceq  16841