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

Theorem necom 2424
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)
Assertion
Ref Expression
necom  |-  ( A  =/=  B  <->  B  =/=  A )

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2172 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2378 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    =/= wne 2340
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 609  ax-in2 610  ax-5 1440  ax-gen 1442  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-ne 2341
This theorem is referenced by:  necomi  2425  necomd  2426  difprsn1  3719  difprsn2  3720  diftpsn3  3721  fndmdifcom  5602  fvpr1  5700  fvpr2  5701  fvpr1g  5702  fvtp1g  5704  fvtp2g  5705  fvtp3g  5706  fvtp2  5708  fvtp3  5709  zltlen  9290  nn0lt2  9293  qltlen  9599  fzofzim  10144  flqeqceilz  10274  isprm2lem  12070  prm2orodd  12080  tridceq  14088
  Copyright terms: Public domain W3C validator