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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2166 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2372 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wb 104  wne 2334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-5 1434  ax-gen 1436  ax-ext 2146
This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-ne 2335
This theorem is referenced by:  necomi  2419  necomd  2420  difprsn1  3707  difprsn2  3708  diftpsn3  3709  fndmdifcom  5586  fvpr1  5684  fvpr2  5685  fvpr1g  5686  fvtp1g  5688  fvtp2g  5689  fvtp3g  5690  fvtp2  5692  fvtp3  5693  zltlen  9261  nn0lt2  9264  qltlen  9570  fzofzim  10114  flqeqceilz  10244  isprm2lem  12037  prm2orodd  12047  tridceq  13797
  Copyright terms: Public domain W3C validator