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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2085 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2287 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wb 103  wne 2249
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 1377  ax-gen 1379  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-ne 2250
This theorem is referenced by:  necomi  2334  necomd  2335  difprsn1  3550  difprsn2  3551  diftpsn3  3552  fndmdifcom  5349  fvpr1  5440  fvpr2  5441  fvpr1g  5442  fvtp1g  5444  fvtp2g  5445  fvtp3g  5446  fvtp2  5448  fvtp3  5449  zltlen  8720  nn0lt2  8723  qltlen  9019  fzofzim  9487  flqeqceilz  9613  isprm2lem  10877  prm2orodd  10887
  Copyright terms: Public domain W3C validator