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

Theorem necomd 3029
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 3027 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 209 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2795  df-ne 2975
This theorem is referenced by:  difsnb  4521  0nelop  5143  xpdifid  5767  difsnen  8275  fofinf1o  8474  en2eleq  9108  en2other2  9109  ackbij1lem15  9335  infpssrlem5  9408  fin23lem24  9423  fin23lem31  9444  isf32lem9  9462  canthnumlem  9749  canthp1lem2  9754  npomex  10097  ltned  10452  lt0ne0  10773  recgt0  11146  zneo  11720  xrltne  12206  supxrbnd  12370  flltnz  12830  seqf1olem1  13057  nn0opthi  13271  hashtpg  13478  hashge3el3dif  13479  cats1un  13693  sumtp  14695  geoserg  14814  geolim  14817  geolim2  14818  tanadd  15111  ruclem6  15178  ruclem7  15179  isprm2lem  15606  isprm5  15630  oddprm  15726  pcmpt  15807  cshwshashlem3  16010  mrissmrcd  16499  estrresOLD  16977  estrres  16978  pmtrprfv  18068  symggen  18085  dprdcntz  18603  dprdres  18623  ablfac1b  18665  lbspss  19283  lspsnnecom  19320  lspindp2l  19336  lspindp2  19337  islbs3  19358  lbsextlem4  19364  sralem  19380  lidlnz  19431  01eq0ring  19475  psrridm  19607  coe1tmfv2  19847  coe1tmmul  19849  uvcf1  20335  frlmup2  20342  dmatmul  20508  mdetralt  20619  mdetunilem2  20624  mdetunilem6  20628  mdetunilem7  20629  maducoeval2  20651  madurid  20655  fvmptnn04ifa  20862  en2top  20997  cmpfi  21419  snfil  21875  tsmsfbas  22138  zcld  22823  iccpnfhmeo  22951  xrhmeo  22952  evth  22965  minveclem3b  23405  i1fres  23680  dvcnvlem  23947  ig1peu  24139  ig1pdvds  24144  aaliou3lem9  24313  taylthlem2  24336  abelthlem2  24394  abelthlem7  24400  tanregt0  24494  logcj  24560  argimgt0  24566  dvloglem  24602  logf1o2  24604  logbrec  24728  ang180lem1  24747  ang180lem2  24748  ang180lem3  24749  ang180lem4  24750  ang180lem5  24751  ang180  24752  isosctrlem3  24758  ssscongptld  24760  angpieqvdlem  24763  angpieqvdlem2  24764  angpieqvd  24766  chordthmlem  24767  chordthmlem2  24768  chordthm  24772  asinneg  24821  ppiltx  25111  perfectlem2  25163  lgsneg  25254  lgsqr  25284  lgseisenlem4  25311  lgsquadlem1  25313  lgsquadlem3  25315  lgsquad2  25319  2lgsoddprm  25349  dchrisum0flblem1  25405  tgbtwnouttr  25600  tgifscgr  25611  tgcgrxfr  25621  tglngval  25654  tgfscgr  25671  tgbtwnconn1lem3  25677  tgbtwnconn3  25680  legtrid  25694  hltr  25713  hlbtwn  25714  btwnhl1  25715  btwnhl  25717  hlcgrex  25719  hlcgreulem  25720  lncom  25725  tgisline  25730  tglineeltr  25734  tglineelsb2  25735  tglinecom  25738  tglinethru  25739  ncolncol  25749  coltr  25750  coltr3  25751  symquadlem  25792  midexlem  25795  ragcol  25802  ragcgr  25810  perpneq  25817  footex  25821  foot  25822  footne  25823  colperpexlem3  25832  mideulem2  25834  opphllem  25835  midex  25837  opphllem1  25847  opphllem2  25848  opphllem3  25849  opphllem4  25850  opphllem5  25851  opphllem6  25852  outpasch  25855  hlpasch  25856  lnopp2hpgb  25863  colhp  25870  lmieu  25884  hypcgrlem1  25899  hypcgrlem2  25900  lnperpex  25903  trgcopy  25904  trgcopyeulem  25905  iscgra1  25910  cgrane2  25913  cgrane3  25914  cgrane4  25915  cgracgr  25918  cgraid  25919  cgraswap  25920  cgrcgra  25921  cgracom  25922  cgratr  25923  cgraswaplr  25924  cgracol  25927  dfcgra2  25929  sacgr  25930  oacgr  25931  acopy  25932  acopyeu  25933  cgrg3col4  25942  tgsas1  25943  tgsas2  25945  tgasa1  25947  tgsss1  25949  isoas  25952  ttgcontlem1  25973  cchhllem  25975  brbtwn2  25993  axlowdimlem15  26044  axlowdimlem16  26045  axcontlem8  26059  upgrex  26195  edglnl  26247  umgrvad2edg  26314  nbupgr  26450  nbumgrvtx  26452  nbgr2vtx1edg  26456  nbuhgr2vtx1edgb  26458  nbupgrres  26475  cplgr3v  26553  cusgrexilem2  26560  usgredgsscusgredg  26577  1hegrvtxdg1r  26626  1egrvtxdg1r  26628  1egrvtxdg0  26629  pthdadjvtx  26848  pthdlem2lem  26885  wspniunwspnon  27057  umgr2cwwk2dif  27209  3pthdlem1  27331  uhgr3cyclex  27349  upgr4cycl4dv4e  27352  frgr3v  27444  1to3vfriswmgr  27449  frgrwopreglem5a  27480  frgrwopreglem3  27483  frgrhash2wsp  27501  staddi  29427  ornglmullt  30126  orngrmullt  30127  orngmullt  30128  ofldlt1  30132  ofldchr  30133  isarchiofld  30136  psgnfzto1stlem  30169  1smat1  30189  submateqlem1  30192  madjusmdetlem2  30213  ordtconnlem1  30289  esumrnmpt2  30449  cntnevol  30610  signstfveq0a  30972  repr0  31008  reprlt  31016  reprinfz1  31019  derangenlem  31470  subfacp1lem1  31478  subfacp1lem3  31481  subfacp1lem5  31483  noseponlem  32132  nosep1o  32147  nosupbnd2lem1  32176  noetalem3  32180  slerec  32238  dfrdg4  32373  ifscgr  32466  cgrxfr  32477  btwnconn1lem8  32516  btwnconn3  32525  segcon2  32527  broutsideof3  32548  outsideoftr  32551  outsideofeq  32552  outsideofeu  32553  lineunray  32569  lineelsb2  32570  linethru  32575  unbdqndv2lem2  32812  knoppndvlem1  32814  knoppndvlem2  32815  knoppndvlem7  32820  knoppndvlem14  32827  bj-bary1lem  33471  bj-bary1lem1  33472  bj-bary1  33473  finxpreclem2  33537  finxp1o  33539  finxpreclem6  33543  fin2solem  33702  poimirlem9  33725  poimirlem15  33731  poimirlem20  33736  poimirlem24  33740  poimirlem25  33741  poimirlem27  33743  itg2addnclem2  33768  ftc1cnnc  33790  heibor1lem  33913  maxidln0  34149  lshpnelb  34758  lsatssn0  34776  lsatcv0  34805  lsat0cv  34807  lsatexch1  34820  l1cvat  34829  atlen0  35084  cvlsupr2  35117  atcvrj2b  35206  2atlt  35213  atbtwn  35220  3noncolr2  35223  4noncolr3  35227  3dimlem3  35235  3dimlem3OLDN  35236  3dimlem4  35238  3dimlem4OLDN  35239  3dim2  35242  1cvratex  35247  1cvrat  35250  ps-1  35251  ps-2  35252  hlatexch4  35255  3atlem4  35260  3atlem6  35262  4atlem0ae  35368  4atlem0be  35369  dalemccnedd  35461  dalemrotps  35465  dalem21  35468  dalem23  35470  dalem27  35473  dalem41  35487  dalem44  35490  dalem54  35500  lnatexN  35553  lnjatN  35554  llnexchb2lem  35642  llnexchb2  35643  lhpn0  35778  lhpexle3lem  35785  lhpmatb  35805  4atexlemswapqr  35837  4atexlemc  35843  4atexlemnclw  35844  4atexlemcnd  35846  4atexlemex4  35847  4atexlemex6  35848  4atex  35850  trlat  35944  trlval4  35963  cdlemc5  35970  cdlemd4  35976  cdlemd7  35979  cdlemd9  35981  cdleme0e  35992  cdleme3b  36004  cdleme3c  36005  cdleme3e  36007  cdleme3h  36010  cdleme7aa  36017  cdleme7e  36022  cdleme7ga  36023  cdleme9  36028  cdleme11c  36036  cdleme11e  36038  cdleme11fN  36039  cdleme11h  36041  cdleme11j  36042  cdleme11k  36043  cdleme15b  36050  cdleme15c  36051  cdleme17c  36063  cdleme18b  36067  cdlemesner  36071  cdleme20zN  36076  cdleme19c  36080  cdleme19d  36081  cdleme19e  36082  cdleme20m  36098  cdleme21a  36100  cdleme21b  36101  cdleme21c  36102  cdleme22f2  36122  cdleme28b  36146  cdleme36a  36235  cdleme36m  36236  cdleme41sn4aw  36250  cdleme43bN  36265  cdleme43dN  36267  cdleme46f2g2  36268  cdleme46f2g1  36269  cdleme4gfv  36282  cdlemeg46nlpq  36292  cdlemeg46req  36304  cdlemeg46fgN  36309  cdlemf1  36336  cdlemg8b  36403  cdlemg9a  36407  cdlemg12g  36424  cdlemg12  36425  cdlemg13a  36426  cdlemg17pq  36447  cdlemg18a  36453  cdlemg18c  36455  cdlemg19a  36458  cdlemg19  36459  cdlemg21  36461  cdlemg31b0N  36469  cdlemg31b0a  36470  cdlemg31c  36474  cdlemg33b0  36476  cdlemg33c0  36477  trlcone  36503  cdlemg42  36504  cdlemg44a  36506  cdlemg46  36510  cdlemh1  36590  cdlemh2  36591  cdlemh  36592  cdlemj3  36598  cdlemk3  36608  cdlemki  36616  cdlemksv2  36622  cdlemk12  36625  cdlemk14  36629  cdlemk15  36630  cdlemk7u  36645  cdlemk11u  36646  cdlemk12u  36647  cdlemk21N  36648  cdlemk20  36649  cdlemk22  36668  cdlemk26-3  36681  cdlemk27-3  36682  cdlemk28-3  36683  cdlemkfid3N  36700  cdlemk11ta  36704  cdlemk47  36724  cdlemk54  36733  dia2dimlem1  36839  dochsat  37158  dochshpncl  37159  lclkrlem2b  37283  lcfrlem21  37338  baerlem5amN  37491  baerlem5bmN  37492  baerlem5abmN  37493  mapdindp4  37498  mapdheq2  37504  mapdheq2biN  37505  mapdh6aN  37510  mapdh6dN  37514  mapdh6eN  37515  mapdh6hN  37518  mapdh7eN  37523  mapdh7dN  37525  mapdh7fN  37526  mapdh8ab  37552  mapdh8ad  37554  mapdh8e  37559  mapdh9a  37564  mapdh9aOLDN  37565  hdmap1l6a  37584  hdmap1l6d  37588  hdmap1l6e  37589  hdmap1l6h  37592  hdmap1eulem  37597  hdmap1eulemOLDN  37598  hdmapval0  37608  hdmapeveclem  37609  hdmapval3lemN  37612  hdmap10lem  37614  hdmap11lem1  37616  hdmaprnlem3N  37625  hdmaprnlem9N  37632  hdmaprnlem3eN  37633  xppss12  37747  jm2.26lem3  38063  rpnnen3lem  38093  rpnnen3  38094  imo72b2lem0  38959  imo72b2lem2  38961  imo72b2lem1  38965  imo72b2  38969  bcc0  39033  chordthmALT  39657  fnchoice  39676  refsum2cnlem1  39684  xrleneltd  40013  xrltned  40047  infleinf  40062  reclt0  40087  icoiccdif  40225  ressiooinf  40258  limcresiooub  40348  limcleqr  40350  limclner  40357  climxrre  40456  icccncfext  40574  cncfiooiccre  40582  dvnxpaek  40631  stoweidlem43  40733  stirlinglem5  40768  stirlinglem7  40770  dirkercncflem1  40793  fourierdlem24  40821  fourierdlem32  40829  fourierdlem33  40830  fourierdlem34  40831  fourierdlem35  40832  fourierdlem46  40842  fourierdlem48  40844  fourierdlem49  40845  fourierdlem64  40860  fourierdlem65  40861  fourierdlem74  40870  fourierdlem76  40872  fourierdlem79  40875  fourierdlem81  40877  fourierdlem91  40887  fourierdlem102  40898  fourierdlem114  40910  etransclem15  40939  etransclem24  40948  sge0rpcpnf  41111  sge0isum  41117  pimrecltpos  41395  pimiooltgt  41397  setsnidel  41916  odz2prm2pw  42044  fmtnoprmfac1lem  42045  fmtnoprmfac1  42046  fmtnoprmfac2  42048  lighneallem1  42091  lighneallem3  42093  perfectALTVlem2  42200  nnsgrpnmnd  42380  nrhmzr  42435  lvecpsslmod  42858
  Copyright terms: Public domain W3C validator