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