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

Theorem necom 2333
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)
Assertion
Ref Expression
necom  |-  ( A  =/=  B  <->  B  =/=  A )

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2085 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2287 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    =/= wne 2249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1377  ax-gen 1379  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-ne 2250
This theorem is referenced by:  necomi  2334  necomd  2335  difprsn1  3550  difprsn2  3551  diftpsn3  3552  fndmdifcom  5350  fvpr1  5441  fvpr2  5442  fvpr1g  5443  fvtp1g  5445  fvtp2g  5446  fvtp3g  5447  fvtp2  5449  fvtp3  5450  zltlen  8721  nn0lt2  8724  qltlen  9020  fzofzim  9488  flqeqceilz  9614  isprm2lem  10878  prm2orodd  10888
  Copyright terms: Public domain W3C validator