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

Theorem neeq1 2295
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
Assertion
Ref Expression
neeq1  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )

Proof of Theorem neeq1
StepHypRef Expression
1 eqeq1 2121 . . 3  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21notbid 639 . 2  |-  ( A  =  B  ->  ( -.  A  =  C  <->  -.  B  =  C ) )
3 df-ne 2283 . 2  |-  ( A  =/=  C  <->  -.  A  =  C )
4 df-ne 2283 . 2  |-  ( B  =/=  C  <->  -.  B  =  C )
52, 3, 43bitr4g 222 1  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104    = wceq 1314    =/= wne 2282
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-ne 2283
This theorem is referenced by:  neeq1i  2297  neeq1d  2300  nelrdva  2860  disji2  3888  0inp0  4050  frecabcl  6250  fiintim  6770  eldju2ndl  6909  updjudhf  6916  xnn0nemnf  8955  uzn0  9243  xrnemnf  9457  xrnepnf  9458  ngtmnft  9493  xsubge0  9557  xposdif  9558  xleaddadd  9563  fztpval  9756  fiinopn  12014
  Copyright terms: Public domain W3C validator