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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2058 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2258 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wb 102  wne 2220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-5 1352  ax-gen 1354  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-ne 2221
This theorem is referenced by:  necomi  2305  necomd  2306  0pss  3292  difprsn1  3530  difprsn2  3531  diftpsn3  3532  fndmdifcom  5300  fvpr1  5392  fvpr2  5393  fvpr1g  5394  fvtp1g  5396  fvtp2g  5397  fvtp3g  5398  fvtp2  5400  fvtp3  5401  zltlen  8376  nn0lt2  8379  qltlen  8671  fzofzim  9145  flqeqceilz  9267
  Copyright terms: Public domain W3C validator