MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necomi Structured version   Unicode version

Theorem necomi 2694
Description: Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
Hypothesis
Ref Expression
necomi.1  |-  A  =/= 
B
Assertion
Ref Expression
necomi  |-  B  =/= 
A

Proof of Theorem necomi
StepHypRef Expression
1 necomi.1 . 2  |-  A  =/= 
B
2 necom 2693 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 208 1  |-  B  =/= 
A
Colors of variables: wff setvar class
Syntax hints:    =/= wne 2606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2436  df-ne 2608
This theorem is referenced by:  0nep0  4463  xp01disj  6936  1sdom  7515  ltneii  9487  0ne1  10389  0ne2  10533  pnfnemnf  11097  mnfnepnf  11098  xmulpnf1  11237  fzprval  11517  hashneq0  12132  hash2pwpr  12182  f1oun2prg  12527  geo2sum2  13334  xpscfn  14497  xpsc0  14498  xpsc1  14499  rescabs  14746  dmdprdpr  16548  dprdpr  16549  mgpress  16602  xpstopnlem1  19382  1sgm2ppw  22539  2sqlem11  22714  axlowdimlem13  23200  usgraexmpldifpr  23318  usgraexmpl  23319  constr3lem4  23533  ex-pss  23635  resvvsca  26302  eulerpartlemgf  26762  sgnnbi  26928  signswch  26962  wepwsolem  29394  refsum2cnlem1  29759  bj-disjsn01  32441  bj-1upln0  32502
  Copyright terms: Public domain W3C validator