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

Theorem necom 2424
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 2172 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2378 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    =/= wne 2340
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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341
This theorem is referenced by:  necomi  2425  necomd  2426  difprsn1  3717  difprsn2  3718  diftpsn3  3719  fndmdifcom  5599  fvpr1  5697  fvpr2  5698  fvpr1g  5699  fvtp1g  5701  fvtp2g  5702  fvtp3g  5703  fvtp2  5705  fvtp3  5706  zltlen  9277  nn0lt2  9280  qltlen  9586  fzofzim  10131  flqeqceilz  10261  isprm2lem  12057  prm2orodd  12067  tridceq  14048
  Copyright terms: Public domain W3C validator