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

Theorem necomi 2541
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 2540 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 199 1  |-  B  =/= 
A
Colors of variables: wff set class
Syntax hints:    =/= wne 2459
This theorem is referenced by:  0nep0  4197  xp01disj  6511  1sdom  7081  ltneii  8947  recgt0ii  9678  pnfnemnf  10475  xrnepnf  10477  xrltnr  10478  nltmnf  10484  xnegmnf  10553  xaddmnf1  10571  xaddmnf2  10572  mnfaddpnf  10574  xaddnepnf  10578  xmullem2  10601  xmulpnf1  10610  xadddilem  10630  fzprval  10860  resup  10987  geo2sum2  12346  prmreclem2  12980  xpscfn  13477  xpsc0  13478  xpsc1  13479  rescabs  13726  setcepi  13936  dmdprdpr  15300  dprdpr  15301  mgpress  15352  xpstopnlem1  17516  i1f1lem  19060  vieta1lem2  19707  mcubic  20159  cubic2  20160  asinlem  20180  sqff1o  20436  1sgm2ppw  20455  dchrpt  20522  lgsqr  20601  2sqlem11  20630  ex-pss  20831  indf1o  23622  konigsberg  23926  axlowdimlem13  24654  ftp  26996  bezoutr1  27176  wepwsolem  27241  mncn0  27447  aaitgo  27470  refsum2cnlem1  27811  f1oun2prg  28187  elprchashprn2  28216  s2f1o  28223  usgraedgprv  28256  usgra1v  28260  usgraexmpldifpr  28266  usgraexmpl  28267  wlkntrllem1  28345  wlkntrllem2  28346  wlkntrllem3  28347  wlkntrllem4  28348  wlkntrllem5  28349  constr3lem2  28392  constr3lem4  28393  constr3lem5  28394  constr3trllem1  28396  constr3trllem3  28398  constr3pthlem1  28401  4cycl4dv  28413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator