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

Theorem necomd 2337
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 2335 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 120 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2251
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 1379  ax-gen 1381  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-ne 2252
This theorem is referenced by:  difsnb  3563  0nelop  4048  frecabcl  6112  fidifsnen  6532  fodjuomnilemdc  6736  en2eleq  6758  en2other2  6759  ltned  7535  lt0ne0  7843  zdceq  8748  zneo  8773  xrlttri3  9192  qdceq  9579  flqltnz  9615  expival  9848  nn0opthd  10019  hashdifpr  10117  isprm2lem  10965
  Copyright terms: Public domain W3C validator