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

Theorem necomd 2335
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necomd  |-  ( ph  ->  B  =/=  A )

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 necom 2333 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 120 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-5 1377  ax-gen 1379  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-ne 2250
This theorem is referenced by:  difsnb  3548  0nelop  4031  frecabcl  6068  fidifsnen  6426  en2eleq  6573  en2other2  6574  ltned  7343  lt0ne0  7651  zdceq  8556  zneo  8581  xrlttri3  9000  qdceq  9385  flqltnz  9421  expival  9627  nn0opthd  9798  hashdifpr  9896  isprm2lem  10705
  Copyright terms: Public domain W3C validator