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  7269  pr1or2  7390  zdceq  9545  nn0lt2  9551  xlesubadd  10108  qdceq  10494  ccat1st1st  11208  swrdccatin1  11296  xrmaxadd  11812  fsumdvds  12393  nn0seqcvgd  12603  pcxnn0cl  12873  pcxqcl  12875  pcge0  12876  pcdvdsb  12883  pcneg  12888  pcdvdstr  12890  pcgcd1  12891  pc2dvds  12893  pcz  12895  pcprmpw2  12896  pcaddlem  12902  pcadd  12903  pcmpt  12906  qexpz  12915  4sqlem19  12972  lgsneg1  15744  lgsdirprm  15753  lgsdir  15754  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  2sqlem9  15843  usgr1e  16080  tridceq  16596