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

Theorem necomd 2413
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 2411 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 121 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2327
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 604  ax-in2 605  ax-5 1427  ax-gen 1429  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-ne 2328
This theorem is referenced by:  difsnb  3700  0nelop  4209  frecabcl  6347  fidifsnen  6816  tpfidisj  6873  omp1eomlem  7039  difinfsnlem  7044  fodjuomnilemdc  7088  en2eleq  7131  en2other2  7132  ltned  7991  lt0ne0  8304  zdceq  9240  zneo  9266  xrlttri3  9705  qdceq  10150  flqltnz  10190  nn0opthd  10600  hashdifpr  10698  sumtp  11315  isprm2lem  11997  oddprm  12138  ennnfonelemex  12185
  Copyright terms: Public domain W3C validator