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

Theorem necom 2444
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 2191 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2398 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 105    =/= 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-in1 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-ne 2361
This theorem is referenced by:  necomi  2445  necomd  2446  difprsn1  3746  difprsn2  3747  diftpsn3  3748  fndmdifcom  5643  fvpr1  5741  fvpr2  5742  fvpr1g  5743  fvtp1g  5745  fvtp2g  5746  fvtp3g  5747  fvtp2  5749  fvtp3  5750  netap  7283  2omotaplemap  7286  zltlen  9361  nn0lt2  9364  qltlen  9670  fzofzim  10218  flqeqceilz  10349  isprm2lem  12148  prm2orodd  12158  tridceq  15266
  Copyright terms: Public domain W3C validator