Theorem dcne 2413

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

Assertion

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

Proof of Theorem dcne

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

Syntax hints:  ¬ wn 3   ↔ wb 105   ∨ wo 715  DECID wdc 841   = wceq 1397   ≠ wne 2402

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 716

This theorem depends on definitions:  df-bi 117  df-dc 842  df-ne 2403

This theorem is referenced by:  updjudhf  7278  pr1or2  7399  zdceq  9555  nn0lt2  9561  xlesubadd  10118  qdceq  10505  ccat1st1st  11222  swrdccatin1  11310  xrmaxadd  11826  fsumdvds  12408  nn0seqcvgd  12618  pcxnn0cl  12888  pcxqcl  12890  pcge0  12891  pcdvdsb  12898  pcneg  12903  pcdvdstr  12905  pcgcd1  12906  pc2dvds  12908  pcz  12910  pcprmpw2  12911  pcaddlem  12917  pcadd  12918  pcmpt  12921  qexpz  12930  4sqlem19  12987  lgsneg1  15760  lgsdirprm  15769  lgsdir  15770  lgsne0  15773  lgsdirnn0  15782  lgsdinn0  15783  2sqlem9  15859  upgr1een  15981  usgr1e  16098  eupth2lem3lem3fi  16327  eupth2lem3lem7fi  16331  tridceq  16687