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

Theorem necomi 2688
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 2687 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 201 1  |-  B  =/= 
A
Colors of variables: wff set class
Syntax hints:    =/= wne 2601
This theorem is referenced by:  0nep0  4372  xp01disj  6742  1sdom  7313  ltneii  9188  pnfnemnf  10719  xrnepnf  10721  xnegmnf  10798  xaddmnf1  10816  xaddmnf2  10817  mnfaddpnf  10819  xaddnepnf  10823  xmullem2  10846  xmulpnf1  10855  xadddilem  10875  fzprval  11108  resup  11250  elprchashprn2  11669  s2f1o  11865  f1oun2prg  11866  geo2sum2  12653  prmreclem2  13287  xpscfn  13786  xpsc0  13787  xpsc1  13788  rescabs  14035  dmdprdpr  15609  dprdpr  15610  mgpress  15661  xpstopnlem1  17843  i1f1lem  19583  mcubic  20689  cubic2  20690  asinlem  20710  sqff1o  20967  1sgm2ppw  20986  dchrpt  21053  lgsqr  21132  2sqlem11  21161  usgra1v  21411  usgraexmpldifpr  21421  usgraexmpl  21422  2trllemH  21554  2trllemE  21555  2wlklemA  21556  2wlklemB  21557  2wlklemC  21558  2trllemD  21559  2trllemG  21560  wlkntrllem1  21561  wlkntrllem2  21562  wlkntrllem3  21563  constr1trl  21590  1pthon  21593  2wlklem1  21599  2pthon  21604  constr3lem2  21635  constr3lem4  21636  constr3lem5  21637  constr3trllem1  21639  constr3trllem3  21641  constr3pthlem1  21644  konigsberg  21711  ex-pss  21738  indf1o  24423  axlowdimlem13  25895  bezoutr1  27053  wepwsolem  27118  mncn0  27323  aaitgo  27346  refsum2cnlem1  27686  f13idfv  28088  usgra2pthspth  28331  usgra2wlkspthlem1  28332  usgra2wlkspthlem2  28333  usgra2pthlem1  28336
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator