Theorem dcne 2388

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 710  DECID wdc 836   = wceq 1373   ≠ wne 2377

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 711

This theorem depends on definitions:  df-bi 117  df-dc 837  df-ne 2378

This theorem is referenced by:  updjudhf  7196  pr1or2  7316  zdceq  9468  nn0lt2  9474  xlesubadd  10025  qdceq  10409  ccat1st1st  11116  xrmaxadd  11647  fsumdvds  12228  nn0seqcvgd  12438  pcxnn0cl  12708  pcxqcl  12710  pcge0  12711  pcdvdsb  12718  pcneg  12723  pcdvdstr  12725  pcgcd1  12726  pc2dvds  12728  pcz  12730  pcprmpw2  12731  pcaddlem  12737  pcadd  12738  pcmpt  12741  qexpz  12750  4sqlem19  12807  lgsneg1  15577  lgsdirprm  15586  lgsdir  15587  lgsne0  15590  lgsdirnn0  15599  lgsdinn0  15600  2sqlem9  15676  tridceq  16136