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 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 105   ∨ wo 720  DECID wdc 846   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

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

This theorem is used by:  updjudhf  7425  pr1or2  7546  zdceq  9729  nn0lt2  9736  xlesubadd  10301  qdceq  10695  ccat1st1st  11430  swrdccatin1  11518  xrmaxadd  12051  fsumdvds  12633  nn0seqcvgd  12843  pcxnn0cl  13117  pcxqcl  13119  pcge0  13120  pcdvdsb  13127  pcneg  13132  pcdvdstr  13134  pcgcd1  13135  pc2dvds  13137  pcz  13139  pcprmpw2  13140  pcaddlem  13146  pcadd  13147  pcmpt  13150  qexpz  13159  4sqlem19  13216  prmlem1a  13249  lgsneg1  16366  lgsdirprm  16375  lgsdir  16376  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  2sqlem9  16465  upgr1een  16587  usgr1e  16704  eupth2lem3lem3fi  16933  eupth2lem3lem7fi  16937  tridceq  17330