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

Theorem necomd 3068
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 3066 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 219 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  difsnb  4731  0nelop  5377  xpdifid  6018  difsnen  8587  fofinf1o  8787  en2eleq  9422  en2other2  9423  ackbij1lem15  9644  infpssrlem5  9717  fin23lem24  9732  fin23lem31  9753  isf32lem9  9771  canthnumlem  10058  canthp1lem2  10063  npomex  10406  ltned  10764  lt0ne0  11094  recgt0  11474  zneo  12053  xrltne  12544  supxrbnd  12709  flltnz  13169  seqf1olem1  13397  nn0opthi  13618  hashtpg  13831  hashge3el3dif  13832  cats1un  14071  sumtp  15092  geoserg  15209  geolim  15214  geolim2  15215  tanadd  15508  ruclem6  15576  ruclem7  15577  isprm2lem  16013  isprm5  16039  oddprm  16135  pcmpt  16216  cshwshashlem3  16419  mrissmrcd  16899  estrres  17377  pmtrprfv  18510  symggen  18527  dprdcntz  19059  dprdres  19079  ablfac1b  19121  lbspss  19783  lspsnnecom  19820  lspindp2l  19835  lspindp2  19836  islbs3  19856  lbsextlem4  19862  sralem  19878  lidlnz  19929  01eq0ring  19973  psrridm  20112  coe1tmfv2  20371  coe1tmmul  20373  uvcf1  20864  frlmup2  20871  dmatmul  21034  mdetralt  21145  mdetunilem2  21150  mdetunilem6  21154  mdetunilem7  21155  maducoeval2  21177  madurid  21181  fvmptnn04ifa  21386  en2top  21521  cmpfi  21944  snfil  22400  tsmsfbas  22663  zcld  23348  iccpnfhmeo  23476  xrhmeo  23477  evth  23490  minveclem3b  23958  i1fres  24233  dvcnvlem  24500  ig1peu  24692  ig1pdvds  24697  aaliou3lem9  24866  taylthlem2  24889  abelthlem2  24947  abelthlem7  24953  cos02pilt1  25038  tanregt0  25050  logcj  25116  argimgt0  25122  dvloglem  25158  logf1o2  25160  logbrec  25287  ang180lem1  25314  ang180lem2  25315  ang180lem3  25316  ang180lem4  25317  ang180lem5  25318  ang180  25319  isosctrlem3  25325  ssscongptld  25327  affineequivne  25332  angpieqvdlem  25333  angpieqvdlem2  25334  angpieqvd  25336  chordthmlem  25337  chordthmlem2  25338  chordthm  25342  asinneg  25391  ppiltx  25681  perfectlem2  25733  lgsneg  25824  lgsqr  25854  lgseisenlem4  25881  lgsquadlem1  25883  lgsquadlem3  25885  lgsquad2  25889  2lgsoddprm  25919  dchrisum0flblem1  26011  tgbtwnouttr  26210  tgifscgr  26221  tgcgrxfr  26231  tglngval  26264  tgfscgr  26281  tgbtwnconn1lem3  26287  tgbtwnconn3  26290  legtrid  26304  hltr  26323  hlbtwn  26324  btwnhl1  26325  btwnhl  26327  hlcgrex  26329  hlcgreulem  26330  lncom  26335  tgisline  26340  tglineeltr  26344  tglineelsb2  26345  tglinecom  26348  tglinethru  26349  ncolncol  26359  coltr  26360  coltr3  26361  symquadlem  26402  midexlem  26405  ragcol  26412  ragcgr  26420  perpneq  26427  footexALT  26431  footexlem1  26432  footexlem2  26433  foot  26435  footne  26436  colperpexlem3  26445  mideulem2  26447  opphllem  26448  midex  26450  opphllem1  26460  opphllem2  26461  opphllem3  26462  opphllem4  26463  opphllem5  26464  opphllem6  26465  outpasch  26468  hlpasch  26469  lnopp2hpgb  26476  colhp  26483  lmieu  26497  hypcgrlem1  26512  hypcgrlem2  26513  lnperpex  26516  trgcopy  26517  trgcopyeulem  26518  iscgra1  26523  cgrane2  26526  cgrane3  26527  cgrane4  26528  cgracgr  26531  cgraid  26532  cgraswap  26533  cgrcgra  26534  cgracom  26535  cgratr  26536  flatcgra  26537  cgraswaplr  26538  cgracol  26541  dfcgra2  26543  sacgr  26544  oacgr  26545  acopy  26546  acopyeu  26547  leagne2  26563  leagne3  26564  cgrg3col4  26566  tgsas1  26567  tgsas2  26569  tgasa1  26571  ttgcontlem1  26598  cchhllem  26600  brbtwn2  26618  axlowdimlem15  26669  axlowdimlem16  26670  axcontlem8  26684  upgrex  26804  edglnl  26855  umgrvad2edg  26922  nbupgr  27053  nbumgrvtx  27055  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  nbupgrres  27073  cplgr3v  27144  cusgrexilem2  27151  usgredgsscusgredg  27168  1hegrvtxdg1r  27217  1egrvtxdg1r  27219  1egrvtxdg0  27220  pthdadjvtx  27438  pthdlem2lem  27475  wspniunwspnon  27629  umgr2cwwk2dif  27770  3pthdlem1  27870  uhgr3cyclex  27888  upgr4cycl4dv4e  27891  frgr3v  27981  1to3vfriswmgr  27986  frgrwopreglem5a  28017  frgrwopreglem3  28020  frgrhash2wsp  28038  staddi  29950  unidifsnne  30223  coprprop  30361  pmtrcnel  30660  pmtrcnel2  30661  psgnfzto1stlem  30669  cycpmco2lem1  30695  cycpmco2  30702  cyc2fvx  30703  cyc3co2  30709  cycpmrn  30712  tocyccntz  30713  cyc3evpm  30719  cyc3genpmlem  30720  ornglmullt  30807  orngrmullt  30808  orngmullt  30809  ofldlt1  30813  ofldchr  30814  isarchiofld  30817  qsidomlem2  30883  1smat1  30968  submateqlem1  30971  madjusmdetlem2  30992  ordtconnlem1  31066  esumrnmpt2  31226  cntnevol  31386  signstfveq0a  31745  repr0  31781  reprlt  31789  reprinfz1  31792  cusgredgex  32265  2cycl2d  32283  acycgr1v  32293  derangenlem  32315  subfacp1lem1  32323  subfacp1lem3  32326  subfacp1lem5  32328  fmlasucdisj  32543  noseponlem  33068  nosep1o  33083  nosupbnd2lem1  33112  noetalem3  33116  slerec  33174  dfrdg4  33309  ifscgr  33402  cgrxfr  33413  btwnconn1lem8  33452  btwnconn3  33461  segcon2  33463  broutsideof3  33484  outsideoftr  33487  outsideofeq  33488  outsideofeu  33489  lineunray  33505  lineelsb2  33506  linethru  33511  unbdqndv2lem2  33746  knoppndvlem1  33748  knoppndvlem2  33749  knoppndvlem7  33754  knoppndvlem14  33761  bj-bary1lem  34479  bj-bary1lem1  34480  bj-bary1  34481  finxpreclem2  34553  finxp1o  34555  finxpreclem6  34559  fin2solem  34759  poimirlem9  34782  poimirlem15  34788  poimirlem20  34793  poimirlem24  34797  poimirlem25  34798  poimirlem27  34800  itg2addnclem2  34825  ftc1cnnc  34847  heibor1lem  34968  maxidln0  35204  lshpnelb  36000  lsatssn0  36018  lsatcv0  36047  lsat0cv  36049  lsatexch1  36062  l1cvat  36071  atlen0  36326  cvlsupr2  36359  atcvrj2b  36448  2atlt  36455  atbtwn  36462  3noncolr2  36465  4noncolr3  36469  3dimlem3  36477  3dimlem3OLDN  36478  3dimlem4  36480  3dimlem4OLDN  36481  3dim2  36484  1cvratex  36489  1cvrat  36492  ps-1  36493  ps-2  36494  hlatexch4  36497  3atlem4  36502  3atlem6  36504  4atlem0ae  36610  4atlem0be  36611  dalemccnedd  36703  dalemrotps  36707  dalem21  36710  dalem23  36712  dalem27  36715  dalem41  36729  dalem44  36732  dalem54  36742  lnatexN  36795  lnjatN  36796  llnexchb2lem  36884  llnexchb2  36885  lhpn0  37020  lhpexle3lem  37027  lhpmatb  37047  4atexlemswapqr  37079  4atexlemc  37085  4atexlemnclw  37086  4atexlemcnd  37088  4atexlemex4  37089  4atexlemex6  37090  4atex  37092  trlat  37185  trlval4  37204  cdlemc5  37211  cdlemd4  37217  cdlemd7  37220  cdlemd9  37222  cdleme0e  37233  cdleme3b  37245  cdleme3c  37246  cdleme3e  37248  cdleme3h  37251  cdleme7aa  37258  cdleme7e  37263  cdleme7ga  37264  cdleme9  37269  cdleme11c  37277  cdleme11e  37279  cdleme11fN  37280  cdleme11h  37282  cdleme11j  37283  cdleme11k  37284  cdleme15b  37291  cdleme15c  37292  cdleme17c  37304  cdleme18b  37308  cdlemesner  37312  cdleme20zN  37317  cdleme19c  37321  cdleme19d  37322  cdleme19e  37323  cdleme20m  37339  cdleme21a  37341  cdleme21b  37342  cdleme21c  37343  cdleme22f2  37363  cdleme28b  37387  cdleme36a  37476  cdleme36m  37477  cdleme41sn4aw  37491  cdleme43bN  37506  cdleme43dN  37508  cdleme46f2g2  37509  cdleme46f2g1  37510  cdleme4gfv  37523  cdlemeg46nlpq  37533  cdlemeg46req  37545  cdlemeg46fgN  37550  cdlemf1  37577  cdlemg8b  37644  cdlemg9a  37648  cdlemg12g  37665  cdlemg12  37666  cdlemg13a  37667  cdlemg17pq  37688  cdlemg18a  37694  cdlemg18c  37696  cdlemg19a  37699  cdlemg19  37700  cdlemg21  37702  cdlemg31b0N  37710  cdlemg31b0a  37711  cdlemg31c  37715  cdlemg33b0  37717  cdlemg33c0  37718  trlcone  37744  cdlemg42  37745  cdlemg44a  37747  cdlemg46  37751  cdlemh1  37831  cdlemh2  37832  cdlemh  37833  cdlemj3  37839  cdlemk3  37849  cdlemki  37857  cdlemksv2  37863  cdlemk12  37866  cdlemk14  37870  cdlemk15  37871  cdlemk7u  37886  cdlemk11u  37887  cdlemk12u  37888  cdlemk21N  37889  cdlemk20  37890  cdlemk22  37909  cdlemk26-3  37922  cdlemk27-3  37923  cdlemk28-3  37924  cdlemkfid3N  37941  cdlemk11ta  37945  cdlemk47  37965  cdlemk54  37974  dia2dimlem1  38080  dochsat  38399  dochshpncl  38400  lclkrlem2b  38524  lcfrlem21  38579  baerlem5amN  38732  baerlem5bmN  38733  baerlem5abmN  38734  mapdindp4  38739  mapdheq2  38745  mapdheq2biN  38746  mapdh6aN  38751  mapdh6dN  38755  mapdh6eN  38756  mapdh6hN  38759  mapdh7eN  38764  mapdh7dN  38766  mapdh7fN  38767  mapdh8ab  38793  mapdh8ad  38795  mapdh8e  38800  mapdh9a  38805  mapdh9aOLDN  38806  hdmap1l6a  38825  hdmap1l6d  38829  hdmap1l6e  38830  hdmap1l6h  38833  hdmap1eulem  38838  hdmap1eulemOLDN  38839  hdmapval0  38849  hdmapeveclem  38850  hdmapval3lemN  38853  hdmap10lem  38855  hdmap11lem1  38857  hdmaprnlem3N  38866  hdmaprnlem9N  38873  hdmaprnlem3eN  38874  xppss12  38993  jm2.26lem3  39476  rpnnen3lem  39506  rpnnen3  39507  imo72b2lem0  40394  imo72b2lem2  40396  imo72b2  40403  mnuprdlem1  40485  bcc0  40549  chordthmALT  41144  fnchoice  41163  refsum2cnlem1  41171  xrleneltd  41467  xrltned  41501  infleinf  41516  reclt0  41539  icoiccdif  41676  ressiooinf  41709  limcresiooub  41799  limcleqr  41801  limclner  41808  climxrre  41907  icccncfext  42046  cncfiooiccre  42054  dvnxpaek  42103  stoweidlem43  42205  stirlinglem5  42240  stirlinglem7  42242  dirkercncflem1  42265  fourierdlem24  42293  fourierdlem32  42301  fourierdlem33  42302  fourierdlem34  42303  fourierdlem35  42304  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem64  42332  fourierdlem65  42333  fourierdlem74  42342  fourierdlem76  42344  fourierdlem79  42347  fourierdlem81  42349  fourierdlem91  42359  fourierdlem102  42370  fourierdlem114  42382  etransclem15  42411  etransclem24  42420  sge0rpcpnf  42580  sge0isum  42586  pimrecltpos  42864  pimiooltgt  42866  setsnidel  43414  odz2prm2pw  43602  fmtnoprmfac1lem  43603  fmtnoprmfac1  43604  fmtnoprmfac2  43606  lighneallem1  43647  lighneallem3  43649  perfectALTVlem2  43764  nnsgrpnmnd  43962  smndex2dnrinv  44015  nrhmzr  44072  lvecpsslmod  44490  affinecomb1  44617  affinecomb2  44618  1subrec1sub  44620  rrx2plord2  44637  line  44647  rrxline  44649  eenglngeehlnmlem2  44653  rrx2vlinest  44656  line2xlem  44668  2itscp  44696
  Copyright terms: Public domain W3C validator