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

Theorem necom 2283
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)
Assertion
Ref Expression
necom (ABBA)

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2039 . 2 (A = BB = A)
21necon3bii 2237 1 (ABBA)
Colors of variables: wff set class
Syntax hints:  wb 98  wne 2201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-5 1333  ax-gen 1335  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-ne 2203
This theorem is referenced by:  necomi  2284  necomd  2285  0pss  3259  difprsn1  3494  difprsn2  3495  diftpsn3  3496  fndmdifcom  5216  fvpr1  5308  fvpr2  5309  fvpr1g  5310  fvtp1g  5312  fvtp2g  5313  fvtp3g  5314  fvtp2  5316  fvtp3  5317  zltlen  8055  nn0lt2  8058  fzofzim  8774
  Copyright terms: Public domain W3C validator