Theorem dcne 2431

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 720  DECID wdc 846   = wceq 1402   ≠ wne 2420

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 721

This theorem depends on definitions:  df-bi 117  df-dc 847  df-ne 2421

This theorem is referenced by:  updjudhf  7409  pr1or2  7530  zdceq  9699  nn0lt2  9706  xlesubadd  10264  qdceq  10657  ccat1st1st  11387  swrdccatin1  11475  xrmaxadd  12005  fsumdvds  12587  nn0seqcvgd  12797  pcxnn0cl  13067  pcxqcl  13069  pcge0  13070  pcdvdsb  13077  pcneg  13082  pcdvdstr  13084  pcgcd1  13085  pc2dvds  13087  pcz  13089  pcprmpw2  13090  pcaddlem  13096  pcadd  13097  pcmpt  13100  qexpz  13109  4sqlem19  13166  lgsneg1  16058  lgsdirprm  16067  lgsdir  16068  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  2sqlem9  16157  upgr1een  16279  usgr1e  16396  eupth2lem3lem3fi  16625  eupth2lem3lem7fi  16629  tridceq  17011