Theorem dcne 2411

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 713  DECID wdc 839   = wceq 1395   ≠ wne 2400

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 714

This theorem depends on definitions:  df-bi 117  df-dc 840  df-ne 2401

This theorem is referenced by:  updjudhf  7242  pr1or2  7363  zdceq  9518  nn0lt2  9524  xlesubadd  10075  qdceq  10459  ccat1st1st  11167  swrdccatin1  11252  xrmaxadd  11767  fsumdvds  12348  nn0seqcvgd  12558  pcxnn0cl  12828  pcxqcl  12830  pcge0  12831  pcdvdsb  12838  pcneg  12843  pcdvdstr  12845  pcgcd1  12846  pc2dvds  12848  pcz  12850  pcprmpw2  12851  pcaddlem  12857  pcadd  12858  pcmpt  12861  qexpz  12870  4sqlem19  12927  lgsneg1  15698  lgsdirprm  15707  lgsdir  15708  lgsne0  15711  lgsdirnn0  15720  lgsdinn0  15721  2sqlem9  15797  tridceq  16383