ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dcne Unicode version

Theorem dcne 2371
Description: Decidable equality expressed in terms of  =/=. Basically the same as df-dc 836. (Contributed by Jim Kingdon, 14-Mar-2020.)
Assertion
Ref Expression
dcne  |-  (DECID  A  =  B  <->  ( A  =  B  \/  A  =/= 
B ) )

Proof of Theorem dcne
StepHypRef Expression
1 df-dc 836 . 2  |-  (DECID  A  =  B  <->  ( A  =  B  \/  -.  A  =  B ) )
2 df-ne 2361 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
32orbi2i 763 . 2  |-  ( ( A  =  B  \/  A  =/=  B )  <->  ( A  =  B  \/  -.  A  =  B )
)
41, 3bitr4i 187 1  |-  (DECID  A  =  B  <->  ( A  =  B  \/  A  =/= 
B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 105    \/ wo 709  DECID wdc 835    = wceq 1364    =/= wne 2360
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 710
This theorem depends on definitions:  df-bi 117  df-dc 836  df-ne 2361
This theorem is referenced by:  updjudhf  7108  zdceq  9358  nn0lt2  9364  xlesubadd  9913  qdceq  10277  xrmaxadd  11301  nn0seqcvgd  12073  pcxnn0cl  12342  pcxqcl  12344  pcge0  12345  pcdvdsb  12352  pcneg  12357  pcdvdstr  12359  pcgcd1  12360  pc2dvds  12362  pcz  12364  pcprmpw2  12365  pcaddlem  12371  pcadd  12372  pcmpt  12375  qexpz  12384  4sqlem19  12441  lgsneg1  14887  lgsdirprm  14896  lgsdir  14897  lgsne0  14900  lgsdirnn0  14909  lgsdinn0  14910  2sqlem9  14932  tridceq  15266
  Copyright terms: Public domain W3C validator