Theorem dcne 2414

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 2404	. . 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 2403

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 2404

This theorem is referenced by:  updjudhf  7321  pr1or2  7442  zdceq  9599  nn0lt2  9605  xlesubadd  10162  qdceq  10550  ccat1st1st  11267  swrdccatin1  11355  xrmaxadd  11884  fsumdvds  12466  nn0seqcvgd  12676  pcxnn0cl  12946  pcxqcl  12948  pcge0  12949  pcdvdsb  12956  pcneg  12961  pcdvdstr  12963  pcgcd1  12964  pc2dvds  12966  pcz  12968  pcprmpw2  12969  pcaddlem  12975  pcadd  12976  pcmpt  12979  qexpz  12988  4sqlem19  13045  lgsneg1  15827  lgsdirprm  15836  lgsdir  15837  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  2sqlem9  15926  upgr1een  16048  usgr1e  16165  eupth2lem3lem3fi  16394  eupth2lem3lem7fi  16398  tridceq  16772