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

Theorem necom 2392
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 2141 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2346 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    =/= wne 2308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-5 1423  ax-gen 1425  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-ne 2309
This theorem is referenced by:  necomi  2393  necomd  2394  difprsn1  3659  difprsn2  3660  diftpsn3  3661  fndmdifcom  5526  fvpr1  5624  fvpr2  5625  fvpr1g  5626  fvtp1g  5628  fvtp2g  5629  fvtp3g  5630  fvtp2  5632  fvtp3  5633  zltlen  9136  nn0lt2  9139  qltlen  9439  fzofzim  9972  flqeqceilz  10098  isprm2lem  11804  prm2orodd  11814
  Copyright terms: Public domain W3C validator