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

Theorem necom 2335
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 2087 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2289 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    =/= wne 2251
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 1379  ax-gen 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-ne 2252
This theorem is referenced by:  necomi  2336  necomd  2337  difprsn1  3559  difprsn2  3560  diftpsn3  3561  fndmdifcom  5368  fvpr1  5462  fvpr2  5463  fvpr1g  5464  fvtp1g  5466  fvtp2g  5467  fvtp3g  5468  fvtp2  5470  fvtp3  5471  zltlen  8758  nn0lt2  8761  qltlen  9057  fzofzim  9527  flqeqceilz  9653  isprm2lem  10980  prm2orodd  10990
  Copyright terms: Public domain W3C validator