Theorem dcne 2356

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 708  DECID wdc 834   = wceq 1353   ≠ wne 2345

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 709

This theorem depends on definitions:  df-bi 117  df-dc 835  df-ne 2346

This theorem is referenced by:  updjudhf  7068  zdceq  9301  nn0lt2  9307  xlesubadd  9854  qdceq  10217  xrmaxadd  11237  nn0seqcvgd  12008  pcxnn0cl  12277  pcge0  12279  pcdvdsb  12286  pcneg  12291  pcdvdstr  12293  pcgcd1  12294  pc2dvds  12296  pcz  12298  pcprmpw2  12299  pcaddlem  12305  pcadd  12306  pcmpt  12308  qexpz  12317  lgsneg1  14006  lgsdirprm  14015  lgsdir  14016  lgsne0  14019  lgsdirnn0  14028  lgsdinn0  14029  2sqlem9  14040  tridceq  14374