Theorem dcne 2346

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

Assertion

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

Proof of Theorem dcne

Step	Hyp	Ref	Expression
1		df-dc 825	. 2 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
2		df-ne 2336	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	orbi2i 752	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵) ↔ (𝐴 = 𝐵 ∨ ¬ 𝐴 = 𝐵))
4	1, 3	bitr4i 186	1 ⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 104   ∨ wo 698  DECID wdc 824   = wceq 1343   ≠ wne 2335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116  df-dc 825  df-ne 2336

This theorem is referenced by:  updjudhf  7040  zdceq  9262  nn0lt2  9268  xlesubadd  9815  qdceq  10178  xrmaxadd  11198  nn0seqcvgd  11969  pcxnn0cl  12238  pcge0  12240  pcdvdsb  12247  pcneg  12252  pcdvdstr  12254  pcgcd1  12255  pc2dvds  12257  pcz  12259  pcprmpw2  12260  pcaddlem  12266  pcadd  12267  pcmpt  12269  qexpz  12278  lgsneg1  13526  lgsdirprm  13535  lgsdir  13536  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  2sqlem9  13560  tridceq  13895