Theorem dcne 2425

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 716  DECID wdc 842   = wceq 1398   ≠ wne 2414

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 717

This theorem depends on definitions:  df-bi 117  df-dc 843  df-ne 2415

This theorem is referenced by:  updjudhf  7383  pr1or2  7504  zdceq  9670  nn0lt2  9677  xlesubadd  10235  qdceq  10628  ccat1st1st  11354  swrdccatin1  11442  xrmaxadd  11971  fsumdvds  12553  nn0seqcvgd  12763  pcxnn0cl  13033  pcxqcl  13035  pcge0  13036  pcdvdsb  13043  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcmpt  13066  qexpz  13075  4sqlem19  13132  lgsneg1  16024  lgsdirprm  16033  lgsdir  16034  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  2sqlem9  16123  upgr1een  16245  usgr1e  16362  eupth2lem3lem3fi  16591  eupth2lem3lem7fi  16595  tridceq  16967