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

Theorem necomd 2691
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 2689 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 199 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-cleq 2414  df-ne 2616
This theorem is referenced by:  difsnb  4142  0nelop  4710  xpdifid  5284  difsnen  7663  fofinf1o  7861  en2eleq  8447  en2other2  8448  ackbij1lem15  8671  infpssrlem5  8744  fin23lem24  8759  fin23lem31  8780  isf32lem9  8798  canthnumlem  9080  canthp1lem2  9085  npomex  9428  ltned  9778  lt0ne0  10087  recgt0  10456  zneo  11025  xrltne  11467  supxrbnd  11621  seqf1olem1  12258  nn0opthi  12462  hashtpg  12645  hashge3el3dif  12646  cats1un  12834  sumtp  13809  geoserg  13923  geolim  13925  geolim2  13926  tanadd  14220  ruclem6  14286  ruclem7  14287  isprm5  14650  oddprm  14764  pcmpt  14836  cshwshashlem3  15067  mrissmrcd  15545  estrres  16023  pmtrprfv  17093  symggen  17110  dprdcntz  17639  dprdres  17660  ablfac1b  17702  lbspss  18304  lspsnnecom  18341  lspindp2l  18356  lspindp2  18357  islbs3  18377  lbsextlem4  18383  sralem  18399  lidlnz  18451  01eq0ring  18495  psrridm  18627  coe1tmfv2  18867  coe1tmmul  18869  uvcf1  19348  frlmup2  19355  dmatmul  19520  mdetralt  19631  mdetunilem2  19636  mdetunilem6  19640  mdetunilem7  19641  maducoeval2  19663  madurid  19667  fvmptnn04ifa  19872  en2top  19999  cmpfi  20421  snfil  20877  tsmsfbas  21140  zcld  21829  iccpnfhmeo  21971  xrhmeo  21972  evth  21985  minveclem3b  22368  minveclem3bOLD  22380  i1fres  22661  dvcnvlem  22926  ig1peu  23120  ig1peuOLD  23121  ig1pdvds  23126  ig1pdvdsOLD  23132  aaliou3lem9  23304  taylthlem2  23327  abelthlem2  23385  abelthlem7  23391  tanregt0  23486  logcj  23553  argimgt0  23559  dvloglem  23591  logf1o2  23593  logbrec  23717  ang180lem1  23736  ang180lem2  23737  ang180lem3  23738  ang180lem4  23739  ang180lem5  23740  ang180  23741  isosctrlem3  23747  ssscongptld  23749  angpieqvdlem  23752  angpieqvdlem2  23753  angpieqvd  23755  chordthmlem  23756  chordthmlem2  23757  chordthm  23761  asinneg  23810  ppiltx  24102  perfectlem2  24156  lgsneg  24245  lgsqr  24272  lgseisenlem4  24278  lgsquadlem1  24280  lgsquadlem3  24282  lgsquad2  24286  dchrisum0flblem1  24344  tgbtwnouttr  24539  tgifscgr  24551  tgcgrxfr  24561  tglngval  24594  tgfscgr  24611  tgbtwnconn1lem3  24617  tgbtwnconn3  24620  legtrid  24634  hltr  24653  hlbtwn  24654  btwnhl1  24655  btwnhl  24657  hlcgrex  24659  hlcgreulem  24660  lncom  24665  tgisline  24670  tglineeltr  24674  tglineelsb2  24675  tglinecom  24678  tglinethru  24679  ncolncol  24689  coltr  24690  coltr3  24691  symquadlem  24732  midexlem  24735  ragcol  24742  ragcgr  24750  perpneq  24757  footex  24761  foot  24762  footne  24763  colperpexlem3  24772  mideulem2  24774  opphllem  24775  midex  24777  opphllem1  24787  opphllem2  24788  opphllem3  24789  opphllem4  24790  opphllem5  24791  opphllem6  24792  outpasch  24795  hlpasch  24796  lnopp2hpgb  24803  colhp  24810  lmieu  24824  hypcgrlem1  24839  hypcgrlem2  24840  lnperpex  24843  trgcopy  24844  trgcopyeulem  24845  iscgra1  24850  cgrane2  24853  cgrane3  24854  cgrane4  24855  cgracgr  24858  cgraid  24859  cgraswap  24860  cgrcgra  24861  cgracom  24862  cgratr  24863  cgraswaplr  24864  cgracol  24867  dfcgra2  24869  sacgr  24870  oacgr  24871  acopy  24872  acopyeu  24873  cgrg3col4  24882  tgsas1  24883  tgsas2  24885  tgasa1  24887  tgsss1  24889  isoas  24892  ttgcontlem1  24913  cchhllem  24915  brbtwn2  24933  axlowdimlem15  24984  axlowdimlem16  24985  axcontlem8  24999  umgraex  25048  isusgra0  25072  usgraop  25075  usgra1v  25115  cyclnspth  25357  4cycl4dv  25393  usg2cwwk2dif  25546  2spot2iun2spont  25617  vdgr1a  25632  eupap1  25702  eupath2lem3  25705  1to3vfriswmgra  25733  frghash2spot  25789  staddi  27897  ornglmullt  28578  orngrmullt  28579  orngmullt  28580  ofldlt1  28584  ofldchr  28585  isarchiofld  28588  psgnfzto1stlem  28621  1smat1  28638  submateqlem1  28641  madjusmdetlem2  28662  ordtconlem1  28738  esumrnmpt2  28897  cntnevol  29058  signstfveq0a  29473  derangenlem  29902  subfacp1lem1  29910  subfacp1lem3  29913  subfacp1lem5  29915  nodenselem3  30577  dfrdg4  30723  ifscgr  30816  cgrxfr  30827  btwnconn1lem8  30866  btwnconn3  30875  segcon2  30877  broutsideof3  30898  outsideoftr  30901  outsideofeq  30902  outsideofeu  30903  lineunray  30919  lineelsb2  30920  linethru  30925  bj-bary1lem  31679  bj-bary1lem1  31680  bj-bary1  31681  finxpreclem2  31746  finxp1o  31748  finxpreclem6  31752  fin2solem  31895  poimirlem9  31913  poimirlem15  31919  poimirlem20  31924  poimirlem24  31928  poimirlem25  31929  poimirlem27  31931  dvtanlemOLD  31955  itg2addnclem2  31958  ftc1cnnc  31980  heibor1lem  32105  maxidln0  32242  lshpnelb  32519  lsatssn0  32537  lsatcv0  32566  lsat0cv  32568  lsatexch1  32581  l1cvat  32590  atlen0  32845  cvlsupr2  32878  atcvrj2b  32966  2atlt  32973  atbtwn  32980  3noncolr2  32983  4noncolr3  32987  3dimlem3  32995  3dimlem3OLDN  32996  3dimlem4  32998  3dimlem4OLDN  32999  3dim2  33002  1cvratex  33007  1cvrat  33010  ps-1  33011  ps-2  33012  hlatexch4  33015  3atlem4  33020  3atlem6  33022  4atlem0ae  33128  4atlem0be  33129  dalemccnedd  33221  dalemrotps  33225  dalem21  33228  dalem23  33230  dalem27  33233  dalem41  33247  dalem44  33250  dalem54  33260  lnatexN  33313  lnjatN  33314  llnexchb2lem  33402  llnexchb2  33403  lhpn0  33538  lhpexle3lem  33545  lhpmatb  33565  4atexlemswapqr  33597  4atexlemc  33603  4atexlemnclw  33604  4atexlemcnd  33606  4atexlemex4  33607  4atexlemex6  33608  4atex  33610  trlat  33704  trlval4  33723  cdlemc5  33730  cdlemd4  33736  cdlemd7  33739  cdlemd9  33741  cdleme0e  33752  cdleme3b  33764  cdleme3c  33765  cdleme3e  33767  cdleme3h  33770  cdleme7aa  33777  cdleme7e  33782  cdleme7ga  33783  cdleme9  33788  cdleme11c  33796  cdleme11e  33798  cdleme11fN  33799  cdleme11h  33801  cdleme11j  33802  cdleme11k  33803  cdleme15b  33810  cdleme15c  33811  cdleme17c  33823  cdleme18b  33827  cdlemesner  33831  cdleme20zN  33836  cdleme19c  33841  cdleme19d  33842  cdleme19e  33843  cdleme20m  33859  cdleme21a  33861  cdleme21b  33862  cdleme21c  33863  cdleme22f2  33883  cdleme28b  33907  cdleme36a  33996  cdleme36m  33997  cdleme41sn4aw  34011  cdleme43bN  34026  cdleme43dN  34028  cdleme46f2g2  34029  cdleme46f2g1  34030  cdleme4gfv  34043  cdlemeg46nlpq  34053  cdlemeg46req  34065  cdlemeg46fgN  34070  cdlemf1  34097  cdlemg8b  34164  cdlemg9a  34168  cdlemg12g  34185  cdlemg12  34186  cdlemg13a  34187  cdlemg17pq  34208  cdlemg18a  34214  cdlemg18c  34216  cdlemg19a  34219  cdlemg19  34220  cdlemg21  34222  cdlemg31b0N  34230  cdlemg31b0a  34231  cdlemg31c  34235  cdlemg33b0  34237  cdlemg33c0  34238  trlcone  34264  cdlemg42  34265  cdlemg44a  34267  cdlemg46  34271  cdlemh1  34351  cdlemh2  34352  cdlemh  34353  cdlemj3  34359  cdlemk3  34369  cdlemki  34377  cdlemksv2  34383  cdlemk12  34386  cdlemk14  34390  cdlemk15  34391  cdlemk7u  34406  cdlemk11u  34407  cdlemk12u  34408  cdlemk21N  34409  cdlemk20  34410  cdlemk22  34429  cdlemk26-3  34442  cdlemk27-3  34443  cdlemk28-3  34444  cdlemkfid3N  34461  cdlemk11ta  34465  cdlemk47  34485  cdlemk54  34494  dia2dimlem1  34601  dochsat  34920  dochshpncl  34921  lclkrlem2b  35045  lcfrlem21  35100  baerlem5amN  35253  baerlem5bmN  35254  baerlem5abmN  35255  mapdindp4  35260  mapdheq2  35266  mapdheq2biN  35267  mapdh6aN  35272  mapdh6dN  35276  mapdh6eN  35277  mapdh6hN  35280  mapdh7eN  35285  mapdh7dN  35287  mapdh7fN  35288  mapdh8ab  35314  mapdh8ad  35316  mapdh8e  35321  mapdh9a  35327  mapdh9aOLDN  35328  hdmap1l6a  35347  hdmap1l6d  35351  hdmap1l6e  35352  hdmap1l6h  35355  hdmap1eulem  35361  hdmap1eulemOLDN  35362  hdmapval0  35373  hdmapeveclem  35374  hdmapval3lemN  35377  hdmap10lem  35379  hdmap11lem1  35381  hdmaprnlem3N  35390  hdmaprnlem9N  35397  hdmaprnlem3eN  35398  jm2.26lem3  35826  rpnnen3lem  35856  rpnnen3  35857  imo72b2lem0  36578  imo72b2lem2  36580  imo72b2lem1  36584  imo72b2  36589  bcc0  36659  chordthmALT  37303  fnchoice  37323  refsum2cnlem1  37331  flltnz  37470  xrleneltd  37500  xrltned  37534  icoiccdif  37574  limcresiooub  37663  limcleqr  37665  limclner  37672  icccncfext  37705  cncfiooiccre  37713  dvnxpaek  37757  stoweidlem43  37844  stirlinglem5  37880  stirlinglem7  37882  dirkercncflem1  37905  fourierdlem24  37933  fourierdlem32  37942  fourierdlem33  37943  fourierdlem34  37944  fourierdlem35  37945  fourierdlem46  37956  fourierdlem48  37958  fourierdlem49  37959  fourierdlem64  37974  fourierdlem65  37975  fourierdlem74  37984  fourierdlem76  37986  fourierdlem79  37989  fourierdlem81  37991  fourierdlem91  38001  fourierdlem102  38012  fourierdlem114  38024  etransclem15  38054  etransclem24  38063  sge0rpcpnf  38171  sge0isum  38177  perfectALTVlem2  38714  structvtxvallem  38952  umgrex  39012  isusgr0  39037  usgr1vr  39106  nbumgr  39179  nbusgrvtx  39181  nbgr2vtx1edg  39183  nbuhgr2vtx1edgb  39185  nbumgrres  39203  cplgr3v  39259  cusgrexi  39264  usgredgsscusgredg  39277  usgvad2edg  39343  nnsgrpnmnd  39438  nrhmzr  39493  lvecpsslmod  39922
  Copyright terms: Public domain W3C validator