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

Theorem necomd 2836
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 2834 . 2 (𝐴𝐵𝐵𝐴)
31, 2sylib 206 1 (𝜑𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781
This theorem is referenced by:  difsnb  4277  0nelop  4879  xpdifid  5466  difsnen  7904  fofinf1o  8103  en2eleq  8691  en2other2  8692  ackbij1lem15  8916  infpssrlem5  8989  fin23lem24  9004  fin23lem31  9025  isf32lem9  9043  canthnumlem  9326  canthp1lem2  9331  npomex  9674  ltned  10024  lt0ne0  10345  recgt0  10718  zneo  11294  xrltne  11831  supxrbnd  11988  flltnz  12431  seqf1olem1  12659  nn0opthi  12876  hashtpg  13073  hashge3el3dif  13074  cats1un  13275  sumtp  14270  geoserg  14385  geolim  14388  geolim2  14389  tanadd  14684  ruclem6  14751  ruclem7  14752  isprm5  15205  oddprm  15301  pcmpt  15382  cshwshashlem3  15590  mrissmrcd  16071  estrres  16550  pmtrprfv  17644  symggen  17661  dprdcntz  18178  dprdres  18198  ablfac1b  18240  lbspss  18851  lspsnnecom  18888  lspindp2l  18903  lspindp2  18904  islbs3  18924  lbsextlem4  18930  sralem  18946  lidlnz  18997  01eq0ring  19041  psrridm  19173  coe1tmfv2  19414  coe1tmmul  19416  uvcf1  19897  frlmup2  19904  dmatmul  20069  mdetralt  20180  mdetunilem2  20185  mdetunilem6  20189  mdetunilem7  20190  maducoeval2  20212  madurid  20216  fvmptnn04ifa  20421  en2top  20547  cmpfi  20968  snfil  21425  tsmsfbas  21688  zcld  22371  iccpnfhmeo  22499  xrhmeo  22500  evth  22513  minveclem3b  22951  i1fres  23222  dvcnvlem  23487  ig1peu  23679  ig1pdvds  23684  aaliou3lem9  23853  taylthlem2  23876  abelthlem2  23934  abelthlem7  23940  tanregt0  24033  logcj  24100  argimgt0  24106  dvloglem  24138  logf1o2  24140  logbrec  24264  ang180lem1  24283  ang180lem2  24284  ang180lem3  24285  ang180lem4  24286  ang180lem5  24287  ang180  24288  isosctrlem3  24294  ssscongptld  24296  angpieqvdlem  24299  angpieqvdlem2  24300  angpieqvd  24302  chordthmlem  24303  chordthmlem2  24304  chordthm  24308  asinneg  24357  ppiltx  24647  perfectlem2  24699  lgsneg  24790  lgsqr  24820  lgseisenlem4  24847  lgsquadlem1  24849  lgsquadlem3  24851  lgsquad2  24855  2lgsoddprm  24885  dchrisum0flblem1  24941  tgbtwnouttr  25136  tgifscgr  25148  tgcgrxfr  25158  tglngval  25191  tgfscgr  25208  tgbtwnconn1lem3  25214  tgbtwnconn3  25217  legtrid  25231  hltr  25250  hlbtwn  25251  btwnhl1  25252  btwnhl  25254  hlcgrex  25256  hlcgreulem  25257  lncom  25262  tgisline  25267  tglineeltr  25271  tglineelsb2  25272  tglinecom  25275  tglinethru  25276  ncolncol  25286  coltr  25287  coltr3  25288  symquadlem  25329  midexlem  25332  ragcol  25339  ragcgr  25347  perpneq  25354  footex  25358  foot  25359  footne  25360  colperpexlem3  25369  mideulem2  25371  opphllem  25372  midex  25374  opphllem1  25384  opphllem2  25385  opphllem3  25386  opphllem4  25387  opphllem5  25388  opphllem6  25389  outpasch  25392  hlpasch  25393  lnopp2hpgb  25400  colhp  25407  lmieu  25421  hypcgrlem1  25436  hypcgrlem2  25437  lnperpex  25440  trgcopy  25441  trgcopyeulem  25442  iscgra1  25447  cgrane2  25450  cgrane3  25451  cgrane4  25452  cgracgr  25455  cgraid  25456  cgraswap  25457  cgrcgra  25458  cgracom  25459  cgratr  25460  cgraswaplr  25461  cgracol  25464  dfcgra2  25466  sacgr  25467  oacgr  25468  acopy  25469  acopyeu  25470  cgrg3col4  25479  tgsas1  25480  tgsas2  25482  tgasa1  25484  tgsss1  25486  isoas  25489  ttgcontlem1  25510  cchhllem  25512  brbtwn2  25530  axlowdimlem15  25581  axlowdimlem16  25582  axcontlem8  25596  umgraex  25645  isusgra0  25669  usgraop  25672  usgra1v  25712  cyclnspth  25952  4cycl4dv  25988  usg2cwwk2dif  26141  2spot2iun2spont  26211  vdgr1a  26226  eupap1  26296  eupath2lem3  26299  1to3vfriswmgra  26327  frghash2spot  26383  staddi  28282  ornglmullt  28931  orngrmullt  28932  orngmullt  28933  ofldlt1  28937  ofldchr  28938  isarchiofld  28941  psgnfzto1stlem  28974  1smat1  28991  submateqlem1  28994  madjusmdetlem2  29015  ordtconlem1  29091  esumrnmpt2  29250  cntnevol  29411  signstfveq0a  29772  derangenlem  30200  subfacp1lem1  30208  subfacp1lem3  30211  subfacp1lem5  30213  noseponlem  30858  nodenselem3  30875  dfrdg4  31021  ifscgr  31114  cgrxfr  31125  btwnconn1lem8  31164  btwnconn3  31173  segcon2  31175  broutsideof3  31196  outsideoftr  31199  outsideofeq  31200  outsideofeu  31201  lineunray  31217  lineelsb2  31218  linethru  31223  unbdqndv2lem2  31464  knoppndvlem1  31466  knoppndvlem2  31467  knoppndvlem7  31472  knoppndvlem14  31479  bj-bary1lem  32120  bj-bary1lem1  32121  bj-bary1  32122  finxpreclem2  32186  finxp1o  32188  finxpreclem6  32192  fin2solem  32348  poimirlem9  32371  poimirlem15  32377  poimirlem20  32382  poimirlem24  32386  poimirlem25  32387  poimirlem27  32389  itg2addnclem2  32415  ftc1cnnc  32437  heibor1lem  32561  maxidln0  32797  lshpnelb  33072  lsatssn0  33090  lsatcv0  33119  lsat0cv  33121  lsatexch1  33134  l1cvat  33143  atlen0  33398  cvlsupr2  33431  atcvrj2b  33519  2atlt  33526  atbtwn  33533  3noncolr2  33536  4noncolr3  33540  3dimlem3  33548  3dimlem3OLDN  33549  3dimlem4  33551  3dimlem4OLDN  33552  3dim2  33555  1cvratex  33560  1cvrat  33563  ps-1  33564  ps-2  33565  hlatexch4  33568  3atlem4  33573  3atlem6  33575  4atlem0ae  33681  4atlem0be  33682  dalemccnedd  33774  dalemrotps  33778  dalem21  33781  dalem23  33783  dalem27  33786  dalem41  33800  dalem44  33803  dalem54  33813  lnatexN  33866  lnjatN  33867  llnexchb2lem  33955  llnexchb2  33956  lhpn0  34091  lhpexle3lem  34098  lhpmatb  34118  4atexlemswapqr  34150  4atexlemc  34156  4atexlemnclw  34157  4atexlemcnd  34159  4atexlemex4  34160  4atexlemex6  34161  4atex  34163  trlat  34257  trlval4  34276  cdlemc5  34283  cdlemd4  34289  cdlemd7  34292  cdlemd9  34294  cdleme0e  34305  cdleme3b  34317  cdleme3c  34318  cdleme3e  34320  cdleme3h  34323  cdleme7aa  34330  cdleme7e  34335  cdleme7ga  34336  cdleme9  34341  cdleme11c  34349  cdleme11e  34351  cdleme11fN  34352  cdleme11h  34354  cdleme11j  34355  cdleme11k  34356  cdleme15b  34363  cdleme15c  34364  cdleme17c  34376  cdleme18b  34380  cdlemesner  34384  cdleme20zN  34389  cdleme19c  34394  cdleme19d  34395  cdleme19e  34396  cdleme20m  34412  cdleme21a  34414  cdleme21b  34415  cdleme21c  34416  cdleme22f2  34436  cdleme28b  34460  cdleme36a  34549  cdleme36m  34550  cdleme41sn4aw  34564  cdleme43bN  34579  cdleme43dN  34581  cdleme46f2g2  34582  cdleme46f2g1  34583  cdleme4gfv  34596  cdlemeg46nlpq  34606  cdlemeg46req  34618  cdlemeg46fgN  34623  cdlemf1  34650  cdlemg8b  34717  cdlemg9a  34721  cdlemg12g  34738  cdlemg12  34739  cdlemg13a  34740  cdlemg17pq  34761  cdlemg18a  34767  cdlemg18c  34769  cdlemg19a  34772  cdlemg19  34773  cdlemg21  34775  cdlemg31b0N  34783  cdlemg31b0a  34784  cdlemg31c  34788  cdlemg33b0  34790  cdlemg33c0  34791  trlcone  34817  cdlemg42  34818  cdlemg44a  34820  cdlemg46  34824  cdlemh1  34904  cdlemh2  34905  cdlemh  34906  cdlemj3  34912  cdlemk3  34922  cdlemki  34930  cdlemksv2  34936  cdlemk12  34939  cdlemk14  34943  cdlemk15  34944  cdlemk7u  34959  cdlemk11u  34960  cdlemk12u  34961  cdlemk21N  34962  cdlemk20  34963  cdlemk22  34982  cdlemk26-3  34995  cdlemk27-3  34996  cdlemk28-3  34997  cdlemkfid3N  35014  cdlemk11ta  35018  cdlemk47  35038  cdlemk54  35047  dia2dimlem1  35154  dochsat  35473  dochshpncl  35474  lclkrlem2b  35598  lcfrlem21  35653  baerlem5amN  35806  baerlem5bmN  35807  baerlem5abmN  35808  mapdindp4  35813  mapdheq2  35819  mapdheq2biN  35820  mapdh6aN  35825  mapdh6dN  35829  mapdh6eN  35830  mapdh6hN  35833  mapdh7eN  35838  mapdh7dN  35840  mapdh7fN  35841  mapdh8ab  35867  mapdh8ad  35869  mapdh8e  35874  mapdh9a  35880  mapdh9aOLDN  35881  hdmap1l6a  35900  hdmap1l6d  35904  hdmap1l6e  35905  hdmap1l6h  35908  hdmap1eulem  35914  hdmap1eulemOLDN  35915  hdmapval0  35926  hdmapeveclem  35927  hdmapval3lemN  35930  hdmap10lem  35932  hdmap11lem1  35934  hdmaprnlem3N  35943  hdmaprnlem9N  35950  hdmaprnlem3eN  35951  jm2.26lem3  36369  rpnnen3lem  36399  rpnnen3  36400  imo72b2lem0  37270  imo72b2lem2  37272  imo72b2lem1  37276  imo72b2  37280  bcc0  37344  chordthmALT  37974  fnchoice  37994  refsum2cnlem1  38002  xrleneltd  38263  xrltned  38297  infleinf  38312  reclt0  38338  icoiccdif  38380  ressiooinf  38414  limcresiooub  38492  limcleqr  38494  limclner  38501  icccncfext  38556  cncfiooiccre  38564  dvnxpaek  38615  stoweidlem43  38719  stirlinglem5  38754  stirlinglem7  38756  dirkercncflem1  38779  fourierdlem24  38807  fourierdlem32  38815  fourierdlem33  38816  fourierdlem34  38817  fourierdlem35  38818  fourierdlem46  38828  fourierdlem48  38830  fourierdlem49  38831  fourierdlem64  38846  fourierdlem65  38847  fourierdlem74  38856  fourierdlem76  38858  fourierdlem79  38861  fourierdlem81  38863  fourierdlem91  38873  fourierdlem102  38884  fourierdlem114  38896  etransclem15  38925  etransclem24  38934  sge0rpcpnf  39097  sge0isum  39103  pimrecltpos  39379  pimiooltgt  39381  odz2prm2pw  39797  fmtnoprmfac1lem  39798  fmtnoprmfac1  39799  fmtnoprmfac2  39801  lighneallem1  39844  lighneallem3  39846  perfectALTVlem2  39949  structvtxvallem  40234  upgrex  40299  umgrvad2edg  40421  nbupgr  40547  nbumgrvtx  40549  nbgr2vtx1edg  40553  nbuhgr2vtx1edgb  40555  nbupgrres  40573  cplgr3v  40638  cusgrexi  40643  usgredgsscusgredg  40656  1hegrvtxdg1r  40705  1egrvtxdg1r  40707  1egrvtxdg0  40708  pthdadjvtx  40917  pthdlem2lem  40954  wspniunwspnon  41111  umgr2cwwk2dif  41229  3pthdlem1  41312  uhgr3cyclex  41330  upgr4cycl4dv4e  41333  frgr3v  41426  1to3vfriswmgr  41431  frgrwopreglem3  41464  frgrhash2wsp  41478  nnsgrpnmnd  41589  nrhmzr  41644  lvecpsslmod  42071
  Copyright terms: Public domain W3C validator