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

Theorem necomi 2713
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 2712 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2mpbi 208 1  |-  B  =/= 
A
Colors of variables: wff setvar class
Syntax hints:    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640
This theorem is referenced by:  nesymi  2716  nesymir  2718  0nep0  4608  xp01disj  7148  1sdom  7724  ltneii  9700  0ne1  10610  0ne2  10754  pnfnemnf  11337  mnfnepnf  11338  xmulpnf1  11477  fzprval  11751  hashneq0  12416  f1oun2prg  12847  geo2sum2  13665  xpscfn  14938  xpsc0  14939  xpsc1  14940  rescabs  15184  dmdprdpr  17077  dprdpr  17078  mgpress  17131  xpstopnlem1  20288  1sgm2ppw  23453  2sqlem11  23628  axlowdimlem13  24235  usgraexmpldifpr  24378  usgraexmpl  24379  constr3lem4  24625  ex-pss  25127  signswch  28496  fprodn0f  31548  bj-disjsn01  34389  bj-1upln0  34450
  Copyright terms: Public domain W3C validator