Theorem dcne 2378

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 709  DECID wdc 835   = wceq 1364   ≠ wne 2367

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 710

This theorem depends on definitions:  df-bi 117  df-dc 836  df-ne 2368

This theorem is referenced by:  updjudhf  7154  zdceq  9420  nn0lt2  9426  xlesubadd  9977  qdceq  10353  xrmaxadd  11445  fsumdvds  12026  nn0seqcvgd  12236  pcxnn0cl  12506  pcxqcl  12508  pcge0  12509  pcdvdsb  12516  pcneg  12521  pcdvdstr  12523  pcgcd1  12524  pc2dvds  12526  pcz  12528  pcprmpw2  12529  pcaddlem  12535  pcadd  12536  pcmpt  12539  qexpz  12548  4sqlem19  12605  lgsneg1  15374  lgsdirprm  15383  lgsdir  15384  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  2sqlem9  15473  tridceq  15813