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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2195 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2402 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  wb 105  wne 2364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-5 1458  ax-gen 1460  ax-ext 2175
This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-ne 2365
This theorem is referenced by:  necomi  2449  necomd  2450  difprsn1  3758  difprsn2  3759  diftpsn3  3760  fndmdifcom  5665  fvpr1  5763  fvpr2  5764  fvpr1g  5765  fvtp1g  5767  fvtp2g  5768  fvtp3g  5769  fvtp2  5771  fvtp3  5772  netap  7316  2omotaplemap  7319  zltlen  9398  nn0lt2  9401  qltlen  9708  fzofzim  10258  flqeqceilz  10392  isprm2lem  12257  prm2orodd  12267  tridceq  15616
  Copyright terms: Public domain W3C validator