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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2024 . 2 (A = BB = A)
21necon3bii 2221 1 (ABBA)
Colors of variables: wff set class
Syntax hints:  wb 98  wne 2186
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 532  ax-in2 533  ax-5 1316  ax-gen 1318  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-ne 2188
This theorem is referenced by:  necomi  2268  necomd  2269  0pss  3242  difprsn1  3477  difprsn2  3478  diftpsn3  3479  fndmdifcom  5198  fvpr1  5290  fvpr2  5291  fvpr1g  5292  fvtp1g  5294  fvtp2g  5295  fvtp3g  5296  fvtp2  5298  fvtp3  5299
  Copyright terms: Public domain W3C validator