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

Theorem necomd 2369
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 2367 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 121 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2283
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 586  ax-in2 587  ax-5 1406  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-ne 2284
This theorem is referenced by:  difsnb  3631  0nelop  4138  frecabcl  6262  fidifsnen  6730  tpfidisj  6782  omp1eomlem  6945  difinfsnlem  6950  fodjuomnilemdc  6982  en2eleq  7015  en2other2  7016  ltned  7841  lt0ne0  8154  zdceq  9080  zneo  9106  xrlttri3  9534  qdceq  9975  flqltnz  10011  nn0opthd  10419  hashdifpr  10517  sumtp  11134  isprm2lem  11704  ennnfonelemex  11833
  Copyright terms: Public domain W3C validator