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

Theorem necomi 2737
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 2736 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 208 1  |-  B  =/= 
A
Colors of variables: wff setvar class
Syntax hints:    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  nesymi  2740  nesymir  2742  0nep0  4618  xp01disj  7146  1sdom  7722  ltneii  9697  0ne1  10603  0ne2  10747  pnfnemnf  11326  mnfnepnf  11327  xmulpnf1  11466  fzprval  11740  hashneq0  12402  hash2pwpr  12485  f1oun2prg  12828  geo2sum2  13646  xpscfn  14814  xpsc0  14815  xpsc1  14816  rescabs  15063  dmdprdpr  16900  dprdpr  16901  mgpress  16954  xpstopnlem1  20073  1sgm2ppw  23231  2sqlem11  23406  axlowdimlem13  23961  usgraexmpldifpr  24104  usgraexmpl  24105  constr3lem4  24351  ex-pss  24854  resvvsca  27515  eulerpartlemgf  27986  sgnnbi  28152  signswch  28186  wepwsolem  30619  refsum2cnlem1  31018  fourierdlem60  31495  fourierdlem61  31496  bj-disjsn01  33605  bj-1upln0  33666
  Copyright terms: Public domain W3C validator