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

Theorem necomd 2878
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 2876 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 208 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  difsnb  4369  0nelop  4989  xpdifid  5597  difsnen  8083  fofinf1o  8282  en2eleq  8869  en2other2  8870  ackbij1lem15  9094  infpssrlem5  9167  fin23lem24  9182  fin23lem31  9203  isf32lem9  9221  canthnumlem  9508  canthp1lem2  9513  npomex  9856  ltned  10211  lt0ne0  10532  recgt0  10905  zneo  11498  xrltne  12032  supxrbnd  12196  flltnz  12652  seqf1olem1  12880  nn0opthi  13097  hashtpg  13305  hashge3el3dif  13306  cats1un  13521  sumtp  14522  geoserg  14642  geolim  14645  geolim2  14646  tanadd  14941  ruclem6  15008  ruclem7  15009  isprm2lem  15441  isprm5  15466  oddprm  15562  pcmpt  15643  cshwshashlem3  15851  mrissmrcd  16347  estrres  16826  pmtrprfv  17919  symggen  17936  dprdcntz  18453  dprdres  18473  ablfac1b  18515  lbspss  19130  lspsnnecom  19167  lspindp2l  19182  lspindp2  19183  islbs3  19203  lbsextlem4  19209  sralem  19225  lidlnz  19276  01eq0ring  19320  psrridm  19452  coe1tmfv2  19693  coe1tmmul  19695  uvcf1  20179  frlmup2  20186  dmatmul  20351  mdetralt  20462  mdetunilem2  20467  mdetunilem6  20471  mdetunilem7  20472  maducoeval2  20494  madurid  20498  fvmptnn04ifa  20703  en2top  20837  cmpfi  21259  snfil  21715  tsmsfbas  21978  zcld  22663  iccpnfhmeo  22791  xrhmeo  22792  evth  22805  minveclem3b  23245  i1fres  23517  dvcnvlem  23784  ig1peu  23976  ig1pdvds  23981  aaliou3lem9  24150  taylthlem2  24173  abelthlem2  24231  abelthlem7  24237  tanregt0  24330  logcj  24397  argimgt0  24403  dvloglem  24439  logf1o2  24441  logbrec  24565  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  ang180lem4  24587  ang180lem5  24588  ang180  24589  isosctrlem3  24595  ssscongptld  24597  angpieqvdlem  24600  angpieqvdlem2  24601  angpieqvd  24603  chordthmlem  24604  chordthmlem2  24605  chordthm  24609  asinneg  24658  ppiltx  24948  perfectlem2  25000  lgsneg  25091  lgsqr  25121  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem3  25152  lgsquad2  25156  2lgsoddprm  25186  dchrisum0flblem1  25242  tgbtwnouttr  25437  tgifscgr  25448  tgcgrxfr  25458  tglngval  25491  tgfscgr  25508  tgbtwnconn1lem3  25514  tgbtwnconn3  25517  legtrid  25531  hltr  25550  hlbtwn  25551  btwnhl1  25552  btwnhl  25554  hlcgrex  25556  hlcgreulem  25557  lncom  25562  tgisline  25567  tglineeltr  25571  tglineelsb2  25572  tglinecom  25575  tglinethru  25576  ncolncol  25586  coltr  25587  coltr3  25588  symquadlem  25629  midexlem  25632  ragcol  25639  ragcgr  25647  perpneq  25654  footex  25658  foot  25659  footne  25660  colperpexlem3  25669  mideulem2  25671  opphllem  25672  midex  25674  opphllem1  25684  opphllem2  25685  opphllem3  25686  opphllem4  25687  opphllem5  25688  opphllem6  25689  outpasch  25692  hlpasch  25693  lnopp2hpgb  25700  colhp  25707  lmieu  25721  hypcgrlem1  25736  hypcgrlem2  25737  lnperpex  25740  trgcopy  25741  trgcopyeulem  25742  iscgra1  25747  cgrane2  25750  cgrane3  25751  cgrane4  25752  cgracgr  25755  cgraid  25756  cgraswap  25757  cgrcgra  25758  cgracom  25759  cgratr  25760  cgraswaplr  25761  cgracol  25764  dfcgra2  25766  sacgr  25767  oacgr  25768  acopy  25769  acopyeu  25770  cgrg3col4  25779  tgsas1  25780  tgsas2  25782  tgasa1  25784  tgsss1  25786  isoas  25789  ttgcontlem1  25810  cchhllem  25812  brbtwn2  25830  axlowdimlem15  25881  axlowdimlem16  25882  axcontlem8  25896  upgrex  26032  edglnl  26083  umgrvad2edg  26150  nbupgr  26285  nbumgrvtx  26287  nbgr2vtx1edg  26291  nbuhgr2vtx1edgb  26293  nbupgrres  26310  cplgr3v  26387  cusgrexilem2  26394  usgredgsscusgredg  26411  1hegrvtxdg1r  26460  1egrvtxdg1r  26462  1egrvtxdg0  26463  pthdadjvtx  26682  pthdlem2lem  26719  wspniunwspnon  26888  umgr2cwwk2dif  27028  3pthdlem1  27142  uhgr3cyclex  27160  upgr4cycl4dv4e  27163  frgr3v  27255  1to3vfriswmgr  27260  frgrwopreglem5a  27291  frgrwopreglem3  27294  frgrhash2wsp  27312  staddi  29233  ornglmullt  29935  orngrmullt  29936  orngmullt  29937  ofldlt1  29941  ofldchr  29942  isarchiofld  29945  psgnfzto1stlem  29978  1smat1  29998  submateqlem1  30001  madjusmdetlem2  30022  ordtconnlem1  30098  esumrnmpt2  30258  cntnevol  30419  signstfveq0a  30781  repr0  30817  reprlt  30825  reprinfz1  30828  derangenlem  31279  subfacp1lem1  31287  subfacp1lem3  31290  subfacp1lem5  31292  noseponlem  31942  nosep1o  31957  nosupbnd2lem1  31986  noetalem3  31990  slerec  32048  dfrdg4  32183  ifscgr  32276  cgrxfr  32287  btwnconn1lem8  32326  btwnconn3  32335  segcon2  32337  broutsideof3  32358  outsideoftr  32361  outsideofeq  32362  outsideofeu  32363  lineunray  32379  lineelsb2  32380  linethru  32385  unbdqndv2lem2  32626  knoppndvlem1  32628  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem14  32641  bj-bary1lem  33290  bj-bary1lem1  33291  bj-bary1  33292  finxpreclem2  33357  finxp1o  33359  finxpreclem6  33363  fin2solem  33525  poimirlem9  33548  poimirlem15  33554  poimirlem20  33559  poimirlem24  33563  poimirlem25  33564  poimirlem27  33566  itg2addnclem2  33592  ftc1cnnc  33614  heibor1lem  33738  maxidln0  33974  lshpnelb  34589  lsatssn0  34607  lsatcv0  34636  lsat0cv  34638  lsatexch1  34651  l1cvat  34660  atlen0  34915  cvlsupr2  34948  atcvrj2b  35036  2atlt  35043  atbtwn  35050  3noncolr2  35053  4noncolr3  35057  3dimlem3  35065  3dimlem3OLDN  35066  3dimlem4  35068  3dimlem4OLDN  35069  3dim2  35072  1cvratex  35077  1cvrat  35080  ps-1  35081  ps-2  35082  hlatexch4  35085  3atlem4  35090  3atlem6  35092  4atlem0ae  35198  4atlem0be  35199  dalemccnedd  35291  dalemrotps  35295  dalem21  35298  dalem23  35300  dalem27  35303  dalem41  35317  dalem44  35320  dalem54  35330  lnatexN  35383  lnjatN  35384  llnexchb2lem  35472  llnexchb2  35473  lhpn0  35608  lhpexle3lem  35615  lhpmatb  35635  4atexlemswapqr  35667  4atexlemc  35673  4atexlemnclw  35674  4atexlemcnd  35676  4atexlemex4  35677  4atexlemex6  35678  4atex  35680  trlat  35774  trlval4  35793  cdlemc5  35800  cdlemd4  35806  cdlemd7  35809  cdlemd9  35811  cdleme0e  35822  cdleme3b  35834  cdleme3c  35835  cdleme3e  35837  cdleme3h  35840  cdleme7aa  35847  cdleme7e  35852  cdleme7ga  35853  cdleme9  35858  cdleme11c  35866  cdleme11e  35868  cdleme11fN  35869  cdleme11h  35871  cdleme11j  35872  cdleme11k  35873  cdleme15b  35880  cdleme15c  35881  cdleme17c  35893  cdleme18b  35897  cdlemesner  35901  cdleme20zN  35906  cdleme19c  35910  cdleme19d  35911  cdleme19e  35912  cdleme20m  35928  cdleme21a  35930  cdleme21b  35931  cdleme21c  35932  cdleme22f2  35952  cdleme28b  35976  cdleme36a  36065  cdleme36m  36066  cdleme41sn4aw  36080  cdleme43bN  36095  cdleme43dN  36097  cdleme46f2g2  36098  cdleme46f2g1  36099  cdleme4gfv  36112  cdlemeg46nlpq  36122  cdlemeg46req  36134  cdlemeg46fgN  36139  cdlemf1  36166  cdlemg8b  36233  cdlemg9a  36237  cdlemg12g  36254  cdlemg12  36255  cdlemg13a  36256  cdlemg17pq  36277  cdlemg18a  36283  cdlemg18c  36285  cdlemg19a  36288  cdlemg19  36289  cdlemg21  36291  cdlemg31b0N  36299  cdlemg31b0a  36300  cdlemg31c  36304  cdlemg33b0  36306  cdlemg33c0  36307  trlcone  36333  cdlemg42  36334  cdlemg44a  36336  cdlemg46  36340  cdlemh1  36420  cdlemh2  36421  cdlemh  36422  cdlemj3  36428  cdlemk3  36438  cdlemki  36446  cdlemksv2  36452  cdlemk12  36455  cdlemk14  36459  cdlemk15  36460  cdlemk7u  36475  cdlemk11u  36476  cdlemk12u  36477  cdlemk21N  36478  cdlemk20  36479  cdlemk22  36498  cdlemk26-3  36511  cdlemk27-3  36512  cdlemk28-3  36513  cdlemkfid3N  36530  cdlemk11ta  36534  cdlemk47  36554  cdlemk54  36563  dia2dimlem1  36670  dochsat  36989  dochshpncl  36990  lclkrlem2b  37114  lcfrlem21  37169  baerlem5amN  37322  baerlem5bmN  37323  baerlem5abmN  37324  mapdindp4  37329  mapdheq2  37335  mapdheq2biN  37336  mapdh6aN  37341  mapdh6dN  37345  mapdh6eN  37346  mapdh6hN  37349  mapdh7eN  37354  mapdh7dN  37356  mapdh7fN  37357  mapdh8ab  37383  mapdh8ad  37385  mapdh8e  37390  mapdh9a  37396  mapdh9aOLDN  37397  hdmap1l6a  37416  hdmap1l6d  37420  hdmap1l6e  37421  hdmap1l6h  37424  hdmap1eulem  37430  hdmap1eulemOLDN  37431  hdmapval0  37442  hdmapeveclem  37443  hdmapval3lemN  37446  hdmap10lem  37448  hdmap11lem1  37450  hdmaprnlem3N  37459  hdmaprnlem9N  37466  hdmaprnlem3eN  37467  jm2.26lem3  37885  rpnnen3lem  37915  rpnnen3  37916  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  bcc0  38856  chordthmALT  39483  fnchoice  39502  refsum2cnlem1  39510  xrleneltd  39852  xrltned  39886  infleinf  39901  reclt0  39927  icoiccdif  40068  ressiooinf  40102  limcresiooub  40192  limcleqr  40194  limclner  40201  climxrre  40300  icccncfext  40418  cncfiooiccre  40426  dvnxpaek  40475  stoweidlem43  40578  stirlinglem5  40613  stirlinglem7  40615  dirkercncflem1  40638  fourierdlem24  40666  fourierdlem32  40674  fourierdlem33  40675  fourierdlem34  40676  fourierdlem35  40677  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem64  40705  fourierdlem65  40706  fourierdlem74  40715  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem91  40732  fourierdlem102  40743  fourierdlem114  40755  etransclem15  40784  etransclem24  40793  sge0rpcpnf  40956  sge0isum  40962  pimrecltpos  41240  pimiooltgt  41242  setsnidel  41672  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnoprmfac1  41802  fmtnoprmfac2  41804  lighneallem1  41847  lighneallem3  41849  perfectALTVlem2  41956  nnsgrpnmnd  42143  nrhmzr  42198  lvecpsslmod  42621
  Copyright terms: Public domain W3C validator