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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2042 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2243 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wb 98  wne 2204
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 1336  ax-gen 1338  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-ne 2206
This theorem is referenced by:  necomi  2290  necomd  2291  0pss  3265  difprsn1  3503  difprsn2  3504  diftpsn3  3505  fndmdifcom  5273  fvpr1  5365  fvpr2  5366  fvpr1g  5367  fvtp1g  5369  fvtp2g  5370  fvtp3g  5371  fvtp2  5373  fvtp3  5374  zltlen  8319  nn0lt2  8322  qltlen  8575  fzofzim  9044  flqeqceilz  9160
  Copyright terms: Public domain W3C validator