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

Theorem necomi 2692
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 2691 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 208 1  |-  B  =/= 
A
Colors of variables: wff setvar class
Syntax hints:    =/= wne 2604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-cleq 2434  df-ne 2606
This theorem is referenced by:  0nep0  4460  xp01disj  6932  1sdom  7511  ltneii  9483  0ne1  10385  0ne2  10529  pnfnemnf  11093  mnfnepnf  11094  xmulpnf1  11233  fzprval  11513  hashneq0  12128  hash2pwpr  12178  f1oun2prg  12523  geo2sum2  13330  xpscfn  14493  xpsc0  14494  xpsc1  14495  rescabs  14742  dmdprdpr  16538  dprdpr  16539  mgpress  16592  xpstopnlem1  19341  1sgm2ppw  22498  2sqlem11  22673  axlowdimlem13  23135  usgraexmpldifpr  23253  usgraexmpl  23254  constr3lem4  23468  ex-pss  23570  resvvsca  26238  eulerpartlemgf  26692  sgnnbi  26858  signswch  26892  wepwsolem  29319  refsum2cnlem1  29684  bj-disjsn01  32171  bj-1upln0  32232
  Copyright terms: Public domain W3C validator