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

Theorem necomd 3076
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
necomd (𝜑𝐵𝐴)

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2 (𝜑𝐴𝐵)
2 necom 3074 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 219 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 3021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-ne 3022
This theorem is referenced by:  difsnb  4738  0nelop  5383  xpdifid  6023  difsnen  8588  fofinf1o  8788  en2eleq  9423  en2other2  9424  ackbij1lem15  9645  infpssrlem5  9718  fin23lem24  9733  fin23lem31  9754  isf32lem9  9772  canthnumlem  10059  canthp1lem2  10064  npomex  10407  ltned  10765  lt0ne0  11095  recgt0  11475  zneo  12054  xrltne  12546  supxrbnd  12711  flltnz  13171  seqf1olem1  13399  nn0opthi  13620  hashtpg  13833  hashge3el3dif  13834  cats1un  14073  sumtp  15094  geoserg  15211  geolim  15216  geolim2  15217  tanadd  15510  ruclem6  15578  ruclem7  15579  isprm2lem  16015  isprm5  16041  oddprm  16137  pcmpt  16218  cshwshashlem3  16421  mrissmrcd  16901  estrres  17379  pmtrprfv  18501  symggen  18518  dprdcntz  19050  dprdres  19070  ablfac1b  19112  lbspss  19774  lspsnnecom  19811  lspindp2l  19826  lspindp2  19827  islbs3  19847  lbsextlem4  19853  sralem  19869  lidlnz  19920  01eq0ring  19964  psrridm  20103  coe1tmfv2  20362  coe1tmmul  20364  uvcf1  20855  frlmup2  20862  dmatmul  21025  mdetralt  21136  mdetunilem2  21141  mdetunilem6  21145  mdetunilem7  21146  maducoeval2  21168  madurid  21172  fvmptnn04ifa  21377  en2top  21512  cmpfi  21935  snfil  22391  tsmsfbas  22654  zcld  23339  iccpnfhmeo  23467  xrhmeo  23468  evth  23481  minveclem3b  23949  i1fres  24224  dvcnvlem  24491  ig1peu  24683  ig1pdvds  24688  aaliou3lem9  24857  taylthlem2  24880  abelthlem2  24938  abelthlem7  24944  tanregt0  25039  logcj  25105  argimgt0  25111  dvloglem  25147  logf1o2  25149  logbrec  25276  ang180lem1  25303  ang180lem2  25304  ang180lem3  25305  ang180lem4  25306  ang180lem5  25307  ang180  25308  isosctrlem3  25314  ssscongptld  25316  affineequivne  25321  angpieqvdlem  25322  angpieqvdlem2  25323  angpieqvd  25325  chordthmlem  25326  chordthmlem2  25327  chordthm  25331  asinneg  25380  ppiltx  25671  perfectlem2  25723  lgsneg  25814  lgsqr  25844  lgseisenlem4  25871  lgsquadlem1  25873  lgsquadlem3  25875  lgsquad2  25879  2lgsoddprm  25909  dchrisum0flblem1  26001  tgbtwnouttr  26200  tgifscgr  26211  tgcgrxfr  26221  tglngval  26254  tgfscgr  26271  tgbtwnconn1lem3  26277  tgbtwnconn3  26280  legtrid  26294  hltr  26313  hlbtwn  26314  btwnhl1  26315  btwnhl  26317  hlcgrex  26319  hlcgreulem  26320  lncom  26325  tgisline  26330  tglineeltr  26334  tglineelsb2  26335  tglinecom  26338  tglinethru  26339  ncolncol  26349  coltr  26350  coltr3  26351  symquadlem  26392  midexlem  26395  ragcol  26402  ragcgr  26410  perpneq  26417  footexALT  26421  footexlem1  26422  footexlem2  26423  foot  26425  footne  26426  colperpexlem3  26435  mideulem2  26437  opphllem  26438  midex  26440  opphllem1  26450  opphllem2  26451  opphllem3  26452  opphllem4  26453  opphllem5  26454  opphllem6  26455  outpasch  26458  hlpasch  26459  lnopp2hpgb  26466  colhp  26473  lmieu  26487  hypcgrlem1  26502  hypcgrlem2  26503  lnperpex  26506  trgcopy  26507  trgcopyeulem  26508  iscgra1  26513  cgrane2  26516  cgrane3  26517  cgrane4  26518  cgracgr  26521  cgraid  26522  cgraswap  26523  cgrcgra  26524  cgracom  26525  cgratr  26526  flatcgra  26527  cgraswaplr  26528  cgracol  26531  dfcgra2  26533  sacgr  26534  oacgr  26535  acopy  26536  acopyeu  26537  leagne2  26553  leagne3  26554  cgrg3col4  26556  tgsas1  26557  tgsas2  26559  tgasa1  26561  ttgcontlem1  26588  cchhllem  26590  brbtwn2  26608  axlowdimlem15  26659  axlowdimlem16  26660  axcontlem8  26674  upgrex  26794  edglnl  26845  umgrvad2edg  26912  nbupgr  27043  nbumgrvtx  27045  nbgr2vtx1edg  27049  nbuhgr2vtx1edgb  27051  nbupgrres  27063  cplgr3v  27134  cusgrexilem2  27141  usgredgsscusgredg  27158  1hegrvtxdg1r  27207  1egrvtxdg1r  27209  1egrvtxdg0  27210  pthdadjvtx  27428  pthdlem2lem  27465  wspniunwspnon  27619  umgr2cwwk2dif  27760  3pthdlem1  27860  uhgr3cyclex  27878  upgr4cycl4dv4e  27881  frgr3v  27971  1to3vfriswmgr  27976  frgrwopreglem5a  28007  frgrwopreglem3  28010  frgrhash2wsp  28028  staddi  29940  unidifsnne  30213  coprprop  30351  pmtrcnel  30650  pmtrcnel2  30651  psgnfzto1stlem  30659  cycpmco2lem1  30685  cycpmco2  30692  cyc2fvx  30693  cyc3co2  30699  cycpmrn  30702  tocyccntz  30703  cyc3evpm  30709  cyc3genpmlem  30710  ornglmullt  30797  orngrmullt  30798  orngmullt  30799  ofldlt1  30803  ofldchr  30804  isarchiofld  30807  qsidomlem2  30873  1smat1  30958  submateqlem1  30961  madjusmdetlem2  30982  ordtconnlem1  31056  esumrnmpt2  31216  cntnevol  31376  signstfveq0a  31735  repr0  31771  reprlt  31779  reprinfz1  31782  cusgredgex  32255  2cycl2d  32273  acycgr1v  32283  derangenlem  32305  subfacp1lem1  32313  subfacp1lem3  32316  subfacp1lem5  32318  fmlasucdisj  32533  noseponlem  33058  nosep1o  33073  nosupbnd2lem1  33102  noetalem3  33106  slerec  33164  dfrdg4  33299  ifscgr  33392  cgrxfr  33403  btwnconn1lem8  33442  btwnconn3  33451  segcon2  33453  broutsideof3  33474  outsideoftr  33477  outsideofeq  33478  outsideofeu  33479  lineunray  33495  lineelsb2  33496  linethru  33501  unbdqndv2lem2  33736  knoppndvlem1  33738  knoppndvlem2  33739  knoppndvlem7  33744  knoppndvlem14  33751  bj-bary1lem  34469  bj-bary1lem1  34470  bj-bary1  34471  finxpreclem2  34543  finxp1o  34545  finxpreclem6  34549  fin2solem  34748  poimirlem9  34771  poimirlem15  34777  poimirlem20  34782  poimirlem24  34786  poimirlem25  34787  poimirlem27  34789  itg2addnclem2  34814  ftc1cnnc  34836  heibor1lem  34958  maxidln0  35194  lshpnelb  35990  lsatssn0  36008  lsatcv0  36037  lsat0cv  36039  lsatexch1  36052  l1cvat  36061  atlen0  36316  cvlsupr2  36349  atcvrj2b  36438  2atlt  36445  atbtwn  36452  3noncolr2  36455  4noncolr3  36459  3dimlem3  36467  3dimlem3OLDN  36468  3dimlem4  36470  3dimlem4OLDN  36471  3dim2  36474  1cvratex  36479  1cvrat  36482  ps-1  36483  ps-2  36484  hlatexch4  36487  3atlem4  36492  3atlem6  36494  4atlem0ae  36600  4atlem0be  36601  dalemccnedd  36693  dalemrotps  36697  dalem21  36700  dalem23  36702  dalem27  36705  dalem41  36719  dalem44  36722  dalem54  36732  lnatexN  36785  lnjatN  36786  llnexchb2lem  36874  llnexchb2  36875  lhpn0  37010  lhpexle3lem  37017  lhpmatb  37037  4atexlemswapqr  37069  4atexlemc  37075  4atexlemnclw  37076  4atexlemcnd  37078  4atexlemex4  37079  4atexlemex6  37080  4atex  37082  trlat  37175  trlval4  37194  cdlemc5  37201  cdlemd4  37207  cdlemd7  37210  cdlemd9  37212  cdleme0e  37223  cdleme3b  37235  cdleme3c  37236  cdleme3e  37238  cdleme3h  37241  cdleme7aa  37248  cdleme7e  37253  cdleme7ga  37254  cdleme9  37259  cdleme11c  37267  cdleme11e  37269  cdleme11fN  37270  cdleme11h  37272  cdleme11j  37273  cdleme11k  37274  cdleme15b  37281  cdleme15c  37282  cdleme17c  37294  cdleme18b  37298  cdlemesner  37302  cdleme20zN  37307  cdleme19c  37311  cdleme19d  37312  cdleme19e  37313  cdleme20m  37329  cdleme21a  37331  cdleme21b  37332  cdleme21c  37333  cdleme22f2  37353  cdleme28b  37377  cdleme36a  37466  cdleme36m  37467  cdleme41sn4aw  37481  cdleme43bN  37496  cdleme43dN  37498  cdleme46f2g2  37499  cdleme46f2g1  37500  cdleme4gfv  37513  cdlemeg46nlpq  37523  cdlemeg46req  37535  cdlemeg46fgN  37540  cdlemf1  37567  cdlemg8b  37634  cdlemg9a  37638  cdlemg12g  37655  cdlemg12  37656  cdlemg13a  37657  cdlemg17pq  37678  cdlemg18a  37684  cdlemg18c  37686  cdlemg19a  37689  cdlemg19  37690  cdlemg21  37692  cdlemg31b0N  37700  cdlemg31b0a  37701  cdlemg31c  37705  cdlemg33b0  37707  cdlemg33c0  37708  trlcone  37734  cdlemg42  37735  cdlemg44a  37737  cdlemg46  37741  cdlemh1  37821  cdlemh2  37822  cdlemh  37823  cdlemj3  37829  cdlemk3  37839  cdlemki  37847  cdlemksv2  37853  cdlemk12  37856  cdlemk14  37860  cdlemk15  37861  cdlemk7u  37876  cdlemk11u  37877  cdlemk12u  37878  cdlemk21N  37879  cdlemk20  37880  cdlemk22  37899  cdlemk26-3  37912  cdlemk27-3  37913  cdlemk28-3  37914  cdlemkfid3N  37931  cdlemk11ta  37935  cdlemk47  37955  cdlemk54  37964  dia2dimlem1  38070  dochsat  38389  dochshpncl  38390  lclkrlem2b  38514  lcfrlem21  38569  baerlem5amN  38722  baerlem5bmN  38723  baerlem5abmN  38724  mapdindp4  38729  mapdheq2  38735  mapdheq2biN  38736  mapdh6aN  38741  mapdh6dN  38745  mapdh6eN  38746  mapdh6hN  38749  mapdh7eN  38754  mapdh7dN  38756  mapdh7fN  38757  mapdh8ab  38783  mapdh8ad  38785  mapdh8e  38790  mapdh9a  38795  mapdh9aOLDN  38796  hdmap1l6a  38815  hdmap1l6d  38819  hdmap1l6e  38820  hdmap1l6h  38823  hdmap1eulem  38828  hdmap1eulemOLDN  38829  hdmapval0  38839  hdmapeveclem  38840  hdmapval3lemN  38843  hdmap10lem  38845  hdmap11lem1  38847  hdmaprnlem3N  38856  hdmaprnlem9N  38863  hdmaprnlem3eN  38864  xppss12  38983  jm2.26lem3  39466  rpnnen3lem  39496  rpnnen3  39497  imo72b2lem0  40384  imo72b2lem2  40386  imo72b2lem1  40390  imo72b2  40394  mnuprdlem1  40476  bcc0  40540  chordthmALT  41135  fnchoice  41154  refsum2cnlem1  41162  xrleneltd  41459  xrltned  41493  infleinf  41508  reclt0  41531  icoiccdif  41668  ressiooinf  41701  limcresiooub  41791  limcleqr  41793  limclner  41800  climxrre  41899  icccncfext  42038  cncfiooiccre  42046  dvnxpaek  42095  stoweidlem43  42197  stirlinglem5  42232  stirlinglem7  42234  dirkercncflem1  42257  fourierdlem24  42285  fourierdlem32  42293  fourierdlem33  42294  fourierdlem34  42295  fourierdlem35  42296  fourierdlem46  42306  fourierdlem48  42308  fourierdlem49  42309  fourierdlem64  42324  fourierdlem65  42325  fourierdlem74  42334  fourierdlem76  42336  fourierdlem79  42339  fourierdlem81  42341  fourierdlem91  42351  fourierdlem102  42362  fourierdlem114  42374  etransclem15  42403  etransclem24  42412  sge0rpcpnf  42572  sge0isum  42578  pimrecltpos  42856  pimiooltgt  42858  setsnidel  43406  odz2prm2pw  43560  fmtnoprmfac1lem  43561  fmtnoprmfac1  43562  fmtnoprmfac2  43564  lighneallem1  43605  lighneallem3  43607  perfectALTVlem2  43722  nnsgrpnmnd  43920  nrhmzr  43979  lvecpsslmod  44397  affinecomb1  44524  affinecomb2  44525  1subrec1sub  44527  rrx2plord2  44544  line  44554  rrxline  44556  eenglngeehlnmlem2  44560  rrx2vlinest  44563  line2xlem  44575  2itscp  44603
  Copyright terms: Public domain W3C validator