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

Theorem necom 2369
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 2119 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2323 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    =/= wne 2285
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 588  ax-in2 589  ax-5 1408  ax-gen 1410  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-ne 2286
This theorem is referenced by:  necomi  2370  necomd  2371  difprsn1  3629  difprsn2  3630  diftpsn3  3631  fndmdifcom  5494  fvpr1  5592  fvpr2  5593  fvpr1g  5594  fvtp1g  5596  fvtp2g  5597  fvtp3g  5598  fvtp2  5600  fvtp3  5601  zltlen  9097  nn0lt2  9100  qltlen  9400  fzofzim  9933  flqeqceilz  10059  isprm2lem  11724  prm2orodd  11734
  Copyright terms: Public domain W3C validator