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  7257  pr1or2  7378  zdceq  9533  nn0lt2  9539  xlesubadd  10091  qdceq  10476  ccat1st1st  11187  swrdccatin1  11272  xrmaxadd  11787  fsumdvds  12368  nn0seqcvgd  12578  pcxnn0cl  12848  pcxqcl  12850  pcge0  12851  pcdvdsb  12858  pcneg  12863  pcdvdstr  12865  pcgcd1  12866  pc2dvds  12868  pcz  12870  pcprmpw2  12871  pcaddlem  12877  pcadd  12878  pcmpt  12881  qexpz  12890  4sqlem19  12947  lgsneg1  15719  lgsdirprm  15728  lgsdir  15729  lgsne0  15732  lgsdirnn0  15741  lgsdinn0  15742  2sqlem9  15818  tridceq  16484