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

Theorem necomd 2433
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 2431 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 122 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2347
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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348
This theorem is referenced by:  difsnb  3734  0nelop  4244  frecabcl  6393  fidifsnen  6863  tpfidisj  6920  omp1eomlem  7086  difinfsnlem  7091  fodjuomnilemdc  7135  en2eleq  7187  en2other2  7188  ltned  8048  lt0ne0  8362  zdceq  9304  zneo  9330  xrlttri3  9771  qdceq  10220  flqltnz  10260  nn0opthd  10673  hashdifpr  10771  sumtp  11393  isprm2lem  12086  oddprm  12229  pcmpt  12311  ennnfonelemex  12385  lgsneg  14058
  Copyright terms: Public domain W3C validator