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

Theorem necomd 2679
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necomd  |-  ( ph  ->  B  =/=  A )

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 necom 2677 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 201 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2622
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-cleq 2445  df-ne 2624
This theorem is referenced by:  difsnb  4083  0nelop  4664  xpdifid  5243  difsnen  7641  fofinf1o  7839  en2eleq  8426  en2other2  8427  ackbij1lem15  8651  infpssrlem5  8724  fin23lem24  8739  fin23lem31  8760  isf32lem9  8778  canthnumlem  9060  canthp1lem2  9065  npomex  9408  ltned  9758  lt0ne0  10069  recgt0  10438  zneo  11008  xrltne  11450  supxrbnd  11604  seqf1olem1  12246  nn0opthi  12450  hashtpg  12636  hashge3el3dif  12637  cats1un  12831  sumtp  13821  geoserg  13935  geolim  13937  geolim2  13938  tanadd  14232  ruclem6  14298  ruclem7  14299  isprm5  14662  oddprm  14776  pcmpt  14848  cshwshashlem3  15079  mrissmrcd  15557  estrres  16035  pmtrprfv  17105  symggen  17122  dprdcntz  17651  dprdres  17672  ablfac1b  17714  lbspss  18316  lspsnnecom  18353  lspindp2l  18368  lspindp2  18369  islbs3  18389  lbsextlem4  18395  sralem  18411  lidlnz  18463  01eq0ring  18507  psrridm  18639  coe1tmfv2  18879  coe1tmmul  18881  uvcf1  19361  frlmup2  19368  dmatmul  19533  mdetralt  19644  mdetunilem2  19649  mdetunilem6  19653  mdetunilem7  19654  maducoeval2  19676  madurid  19680  fvmptnn04ifa  19885  en2top  20012  cmpfi  20434  snfil  20890  tsmsfbas  21153  zcld  21842  iccpnfhmeo  21984  xrhmeo  21985  evth  21998  minveclem3b  22381  minveclem3bOLD  22393  i1fres  22675  dvcnvlem  22940  ig1peu  23134  ig1peuOLD  23135  ig1pdvds  23140  ig1pdvdsOLD  23146  aaliou3lem9  23318  taylthlem2  23341  abelthlem2  23399  abelthlem7  23405  tanregt0  23500  logcj  23567  argimgt0  23573  dvloglem  23605  logf1o2  23607  logbrec  23731  ang180lem1  23750  ang180lem2  23751  ang180lem3  23752  ang180lem4  23753  ang180lem5  23754  ang180  23755  isosctrlem3  23761  ssscongptld  23763  angpieqvdlem  23766  angpieqvdlem2  23767  angpieqvd  23769  chordthmlem  23770  chordthmlem2  23771  chordthm  23775  asinneg  23824  ppiltx  24116  perfectlem2  24170  lgsneg  24259  lgsqr  24286  lgseisenlem4  24292  lgsquadlem1  24294  lgsquadlem3  24296  lgsquad2  24300  dchrisum0flblem1  24358  tgbtwnouttr  24553  tgifscgr  24565  tgcgrxfr  24575  tglngval  24608  tgfscgr  24625  tgbtwnconn1lem3  24631  tgbtwnconn3  24634  legtrid  24648  hltr  24667  hlbtwn  24668  btwnhl1  24669  btwnhl  24671  hlcgrex  24673  hlcgreulem  24674  lncom  24679  tgisline  24684  tglineeltr  24688  tglineelsb2  24689  tglinecom  24692  tglinethru  24693  ncolncol  24703  coltr  24704  coltr3  24705  symquadlem  24746  midexlem  24749  ragcol  24756  ragcgr  24764  perpneq  24771  footex  24775  foot  24776  footne  24777  colperpexlem3  24786  mideulem2  24788  opphllem  24789  midex  24791  opphllem1  24801  opphllem2  24802  opphllem3  24803  opphllem4  24804  opphllem5  24805  opphllem6  24806  outpasch  24809  hlpasch  24810  lnopp2hpgb  24817  colhp  24824  lmieu  24838  hypcgrlem1  24853  hypcgrlem2  24854  lnperpex  24857  trgcopy  24858  trgcopyeulem  24859  iscgra1  24864  cgrane2  24867  cgrane3  24868  cgrane4  24869  cgracgr  24872  cgraid  24873  cgraswap  24874  cgrcgra  24875  cgracom  24876  cgratr  24877  cgraswaplr  24878  cgracol  24881  dfcgra2  24883  sacgr  24884  oacgr  24885  acopy  24886  acopyeu  24887  cgrg3col4  24896  tgsas1  24897  tgsas2  24899  tgasa1  24901  tgsss1  24903  isoas  24906  ttgcontlem1  24927  cchhllem  24929  brbtwn2  24947  axlowdimlem15  24998  axlowdimlem16  24999  axcontlem8  25013  umgraex  25062  isusgra0  25086  usgraop  25089  usgra1v  25129  cyclnspth  25371  4cycl4dv  25407  usg2cwwk2dif  25560  2spot2iun2spont  25631  vdgr1a  25646  eupap1  25716  eupath2lem3  25719  1to3vfriswmgra  25747  frghash2spot  25803  staddi  27911  ornglmullt  28577  orngrmullt  28578  orngmullt  28579  ofldlt1  28583  ofldchr  28584  isarchiofld  28587  psgnfzto1stlem  28620  1smat1  28637  submateqlem1  28640  madjusmdetlem2  28661  ordtconlem1  28737  esumrnmpt2  28896  cntnevol  29057  signstfveq0a  29471  derangenlem  29900  subfacp1lem1  29908  subfacp1lem3  29911  subfacp1lem5  29913  noseponlem  30561  nodenselem3  30578  dfrdg4  30724  ifscgr  30817  cgrxfr  30828  btwnconn1lem8  30867  btwnconn3  30876  segcon2  30878  broutsideof3  30899  outsideoftr  30902  outsideofeq  30903  outsideofeu  30904  lineunray  30920  lineelsb2  30921  linethru  30926  bj-bary1lem  31717  bj-bary1lem1  31718  bj-bary1  31719  finxpreclem2  31784  finxp1o  31786  finxpreclem6  31790  fin2solem  31933  poimirlem9  31951  poimirlem15  31957  poimirlem20  31962  poimirlem24  31966  poimirlem25  31967  poimirlem27  31969  dvtanlemOLD  31993  itg2addnclem2  31996  ftc1cnnc  32018  heibor1lem  32143  maxidln0  32280  lshpnelb  32552  lsatssn0  32570  lsatcv0  32599  lsat0cv  32601  lsatexch1  32614  l1cvat  32623  atlen0  32878  cvlsupr2  32911  atcvrj2b  32999  2atlt  33006  atbtwn  33013  3noncolr2  33016  4noncolr3  33020  3dimlem3  33028  3dimlem3OLDN  33029  3dimlem4  33031  3dimlem4OLDN  33032  3dim2  33035  1cvratex  33040  1cvrat  33043  ps-1  33044  ps-2  33045  hlatexch4  33048  3atlem4  33053  3atlem6  33055  4atlem0ae  33161  4atlem0be  33162  dalemccnedd  33254  dalemrotps  33258  dalem21  33261  dalem23  33263  dalem27  33266  dalem41  33280  dalem44  33283  dalem54  33293  lnatexN  33346  lnjatN  33347  llnexchb2lem  33435  llnexchb2  33436  lhpn0  33571  lhpexle3lem  33578  lhpmatb  33598  4atexlemswapqr  33630  4atexlemc  33636  4atexlemnclw  33637  4atexlemcnd  33639  4atexlemex4  33640  4atexlemex6  33641  4atex  33643  trlat  33737  trlval4  33756  cdlemc5  33763  cdlemd4  33769  cdlemd7  33772  cdlemd9  33774  cdleme0e  33785  cdleme3b  33797  cdleme3c  33798  cdleme3e  33800  cdleme3h  33803  cdleme7aa  33810  cdleme7e  33815  cdleme7ga  33816  cdleme9  33821  cdleme11c  33829  cdleme11e  33831  cdleme11fN  33832  cdleme11h  33834  cdleme11j  33835  cdleme11k  33836  cdleme15b  33843  cdleme15c  33844  cdleme17c  33856  cdleme18b  33860  cdlemesner  33864  cdleme20zN  33869  cdleme19c  33874  cdleme19d  33875  cdleme19e  33876  cdleme20m  33892  cdleme21a  33894  cdleme21b  33895  cdleme21c  33896  cdleme22f2  33916  cdleme28b  33940  cdleme36a  34029  cdleme36m  34030  cdleme41sn4aw  34044  cdleme43bN  34059  cdleme43dN  34061  cdleme46f2g2  34062  cdleme46f2g1  34063  cdleme4gfv  34076  cdlemeg46nlpq  34086  cdlemeg46req  34098  cdlemeg46fgN  34103  cdlemf1  34130  cdlemg8b  34197  cdlemg9a  34201  cdlemg12g  34218  cdlemg12  34219  cdlemg13a  34220  cdlemg17pq  34241  cdlemg18a  34247  cdlemg18c  34249  cdlemg19a  34252  cdlemg19  34253  cdlemg21  34255  cdlemg31b0N  34263  cdlemg31b0a  34264  cdlemg31c  34268  cdlemg33b0  34270  cdlemg33c0  34271  trlcone  34297  cdlemg42  34298  cdlemg44a  34300  cdlemg46  34304  cdlemh1  34384  cdlemh2  34385  cdlemh  34386  cdlemj3  34392  cdlemk3  34402  cdlemki  34410  cdlemksv2  34416  cdlemk12  34419  cdlemk14  34423  cdlemk15  34424  cdlemk7u  34439  cdlemk11u  34440  cdlemk12u  34441  cdlemk21N  34442  cdlemk20  34443  cdlemk22  34462  cdlemk26-3  34475  cdlemk27-3  34476  cdlemk28-3  34477  cdlemkfid3N  34494  cdlemk11ta  34498  cdlemk47  34518  cdlemk54  34527  dia2dimlem1  34634  dochsat  34953  dochshpncl  34954  lclkrlem2b  35078  lcfrlem21  35133  baerlem5amN  35286  baerlem5bmN  35287  baerlem5abmN  35288  mapdindp4  35293  mapdheq2  35299  mapdheq2biN  35300  mapdh6aN  35305  mapdh6dN  35309  mapdh6eN  35310  mapdh6hN  35313  mapdh7eN  35318  mapdh7dN  35320  mapdh7fN  35321  mapdh8ab  35347  mapdh8ad  35349  mapdh8e  35354  mapdh9a  35360  mapdh9aOLDN  35361  hdmap1l6a  35380  hdmap1l6d  35384  hdmap1l6e  35385  hdmap1l6h  35388  hdmap1eulem  35394  hdmap1eulemOLDN  35395  hdmapval0  35406  hdmapeveclem  35407  hdmapval3lemN  35410  hdmap10lem  35412  hdmap11lem1  35414  hdmaprnlem3N  35423  hdmaprnlem9N  35430  hdmaprnlem3eN  35431  jm2.26lem3  35858  rpnnen3lem  35888  rpnnen3  35889  imo72b2lem0  36610  imo72b2lem2  36612  imo72b2lem1  36616  imo72b2  36620  bcc0  36690  chordthmALT  37327  fnchoice  37347  refsum2cnlem1  37355  flltnz  37547  xrleneltd  37577  xrltned  37611  infleinf  37627  icoiccdif  37666  limcresiooub  37765  limcleqr  37767  limclner  37774  icccncfext  37807  cncfiooiccre  37815  dvnxpaek  37859  stoweidlem43  37961  stirlinglem5  37997  stirlinglem7  37999  dirkercncflem1  38022  fourierdlem24  38050  fourierdlem32  38059  fourierdlem33  38060  fourierdlem34  38061  fourierdlem35  38062  fourierdlem46  38073  fourierdlem48  38075  fourierdlem49  38076  fourierdlem64  38091  fourierdlem65  38092  fourierdlem74  38101  fourierdlem76  38103  fourierdlem79  38106  fourierdlem81  38108  fourierdlem91  38118  fourierdlem102  38129  fourierdlem114  38141  etransclem15  38171  etransclem24  38180  sge0rpcpnf  38322  sge0isum  38328  perfectALTVlem2  38935  structvtxvallem  39220  upgrex  39283  usgr1vr  39431  nbupgr  39514  nbumgrvtx  39516  nbgr2vtx1edg  39520  nbuhgr2vtx1edgb  39522  nbupgrres  39540  cplgr3v  39604  cusgrexi  39609  usgredgsscusgredg  39622  pthdadjvtx  39815  pthdlem2lem  39845  3pthdlem1  39957  uhgr3cyclex  39975  upgr4cycl4dv4e  39978  usgvad2edg  40048  nnsgrpnmnd  40143  nrhmzr  40198  lvecpsslmod  40625
  Copyright terms: Public domain W3C validator