Theorem necomd 3071

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

Step	Hyp	Ref	Expression
1		necomd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		necom 3069	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 220	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-ne 3017

This theorem is referenced by:  difsnb  4739  0nelop  5386  xpdifid  6025  difsnen  8599  fofinf1o  8799  en2eleq  9434  en2other2  9435  ackbij1lem15  9656  infpssrlem5  9729  fin23lem24  9744  fin23lem31  9765  isf32lem9  9783  canthnumlem  10070  canthp1lem2  10075  npomex  10418  ltned  10776  lt0ne0  11106  recgt0  11486  zneo  12066  xrltne  12557  supxrbnd  12722  flltnz  13182  seqf1olem1  13410  nn0opthi  13631  hashtpg  13844  hashge3el3dif  13845  cats1un  14083  sumtp  15104  geoserg  15221  geolim  15226  geolim2  15227  tanadd  15520  ruclem6  15588  ruclem7  15589  isprm2lem  16025  isprm5  16051  oddprm  16147  pcmpt  16228  cshwshashlem3  16431  mrissmrcd  16911  estrres  17389  smndex2dnrinv  18080  pmtrprfv  18581  symggen  18598  dprdcntz  19130  dprdres  19150  ablfac1b  19192  lbspss  19854  lspsnnecom  19891  lspindp2l  19906  lspindp2  19907  islbs3  19927  lbsextlem4  19933  sralem  19949  lidlnz  20001  01eq0ring  20045  psrridm  20184  coe1tmfv2  20443  coe1tmmul  20445  uvcf1  20936  frlmup2  20943  dmatmul  21106  mdetralt  21217  mdetunilem2  21222  mdetunilem6  21226  mdetunilem7  21227  maducoeval2  21249  madurid  21253  fvmptnn04ifa  21458  en2top  21593  cmpfi  22016  snfil  22472  tsmsfbas  22736  zcld  23421  iccpnfhmeo  23549  xrhmeo  23550  evth  23563  minveclem3b  24031  i1fres  24306  dvcnvlem  24573  ig1peu  24765  ig1pdvds  24770  aaliou3lem9  24939  taylthlem2  24962  abelthlem2  25020  abelthlem7  25026  cos02pilt1  25111  tanregt0  25123  logcj  25189  argimgt0  25195  dvloglem  25231  logf1o2  25233  logbrec  25360  ang180lem1  25387  ang180lem2  25388  ang180lem3  25389  ang180lem4  25390  ang180lem5  25391  ang180  25392  isosctrlem3  25398  ssscongptld  25400  affineequivne  25405  angpieqvdlem  25406  angpieqvdlem2  25407  angpieqvd  25409  chordthmlem  25410  chordthmlem2  25411  chordthm  25415  asinneg  25464  ppiltx  25754  perfectlem2  25806  lgsneg  25897  lgsqr  25927  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem3  25958  lgsquad2  25962  2lgsoddprm  25992  dchrisum0flblem1  26084  tgbtwnouttr  26283  tgifscgr  26294  tgcgrxfr  26304  tglngval  26337  tgfscgr  26354  tgbtwnconn1lem3  26360  tgbtwnconn3  26363  legtrid  26377  hltr  26396  hlbtwn  26397  btwnhl1  26398  btwnhl  26400  hlcgrex  26402  hlcgreulem  26403  lncom  26408  tgisline  26413  tglineeltr  26417  tglineelsb2  26418  tglinecom  26421  tglinethru  26422  ncolncol  26432  coltr  26433  coltr3  26434  symquadlem  26475  midexlem  26478  ragcol  26485  ragcgr  26493  perpneq  26500  footexALT  26504  footexlem1  26505  footexlem2  26506  foot  26508  footne  26509  colperpexlem3  26518  mideulem2  26520  opphllem  26521  midex  26523  opphllem1  26533  opphllem2  26534  opphllem3  26535  opphllem4  26536  opphllem5  26537  opphllem6  26538  outpasch  26541  hlpasch  26542  lnopp2hpgb  26549  colhp  26556  lmieu  26570  hypcgrlem1  26585  hypcgrlem2  26586  lnperpex  26589  trgcopy  26590  trgcopyeulem  26591  iscgra1  26596  cgrane2  26599  cgrane3  26600  cgrane4  26601  cgracgr  26604  cgraid  26605  cgraswap  26606  cgrcgra  26607  cgracom  26608  cgratr  26609  flatcgra  26610  cgraswaplr  26611  cgracol  26614  dfcgra2  26616  sacgr  26617  oacgr  26618  acopy  26619  acopyeu  26620  leagne2  26636  leagne3  26637  cgrg3col4  26639  tgsas1  26640  tgsas2  26642  tgasa1  26644  ttgcontlem1  26671  cchhllem  26673  brbtwn2  26691  axlowdimlem15  26742  axlowdimlem16  26743  axcontlem8  26757  upgrex  26877  edglnl  26928  umgrvad2edg  26995  nbupgr  27126  nbumgrvtx  27128  nbgr2vtx1edg  27132  nbuhgr2vtx1edgb  27134  nbupgrres  27146  cplgr3v  27217  cusgrexilem2  27224  usgredgsscusgredg  27241  1hegrvtxdg1r  27290  1egrvtxdg1r  27292  1egrvtxdg0  27293  pthdadjvtx  27511  pthdlem2lem  27548  wspniunwspnon  27702  umgr2cwwk2dif  27843  3pthdlem1  27943  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  frgr3v  28054  1to3vfriswmgr  28059  frgrwopreglem5a  28090  frgrwopreglem3  28093  frgrhash2wsp  28111  staddi  30023  unidifsnne  30296  coprprop  30435  pmtrcnel  30733  pmtrcnel2  30734  psgnfzto1stlem  30742  cycpmco2lem1  30768  cycpmco2  30775  cyc2fvx  30776  cyc3co2  30782  cycpmrn  30785  tocyccntz  30786  cyc3evpm  30792  cyc3genpmlem  30793  ornglmullt  30880  orngrmullt  30881  orngmullt  30882  ofldlt1  30886  ofldchr  30887  isarchiofld  30890  qsidomlem2  30966  mxidlnzr  30976  1smat1  31069  submateqlem1  31072  madjusmdetlem2  31093  ordtconnlem1  31167  esumrnmpt2  31327  cntnevol  31487  signstfveq0a  31846  repr0  31882  reprlt  31890  reprinfz1  31893  cusgredgex  32368  2cycl2d  32386  acycgr1v  32396  derangenlem  32418  subfacp1lem1  32426  subfacp1lem3  32429  subfacp1lem5  32431  fmlasucdisj  32646  noseponlem  33171  nosep1o  33186  nosupbnd2lem1  33215  noetalem3  33219  slerec  33277  dfrdg4  33412  ifscgr  33505  cgrxfr  33516  btwnconn1lem8  33555  btwnconn3  33564  segcon2  33566  broutsideof3  33587  outsideoftr  33590  outsideofeq  33591  outsideofeu  33592  lineunray  33608  lineelsb2  33609  linethru  33614  unbdqndv2lem2  33849  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem14  33864  bj-bary1lem  34594  bj-bary1lem1  34595  bj-bary1  34596  finxpreclem2  34674  finxp1o  34676  finxpreclem6  34680  fin2solem  34893  poimirlem9  34916  poimirlem15  34922  poimirlem20  34927  poimirlem24  34931  poimirlem25  34932  poimirlem27  34934  itg2addnclem2  34959  ftc1cnnc  34981  heibor1lem  35102  maxidln0  35338  lshpnelb  36135  lsatssn0  36153  lsatcv0  36182  lsat0cv  36184  lsatexch1  36197  l1cvat  36206  atlen0  36461  cvlsupr2  36494  atcvrj2b  36583  2atlt  36590  atbtwn  36597  3noncolr2  36600  4noncolr3  36604  3dimlem3  36612  3dimlem3OLDN  36613  3dimlem4  36615  3dimlem4OLDN  36616  3dim2  36619  1cvratex  36624  1cvrat  36627  ps-1  36628  ps-2  36629  hlatexch4  36632  3atlem4  36637  3atlem6  36639  4atlem0ae  36745  4atlem0be  36746  dalemccnedd  36838  dalemrotps  36842  dalem21  36845  dalem23  36847  dalem27  36850  dalem41  36864  dalem44  36867  dalem54  36877  lnatexN  36930  lnjatN  36931  llnexchb2lem  37019  llnexchb2  37020  lhpn0  37155  lhpexle3lem  37162  lhpmatb  37182  4atexlemswapqr  37214  4atexlemc  37220  4atexlemnclw  37221  4atexlemcnd  37223  4atexlemex4  37224  4atexlemex6  37225  4atex  37227  trlat  37320  trlval4  37339  cdlemc5  37346  cdlemd4  37352  cdlemd7  37355  cdlemd9  37357  cdleme0e  37368  cdleme3b  37380  cdleme3c  37381  cdleme3e  37383  cdleme3h  37386  cdleme7aa  37393  cdleme7e  37398  cdleme7ga  37399  cdleme9  37404  cdleme11c  37412  cdleme11e  37414  cdleme11fN  37415  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme15b  37426  cdleme15c  37427  cdleme17c  37439  cdleme18b  37443  cdlemesner  37447  cdleme20zN  37452  cdleme19c  37456  cdleme19d  37457  cdleme19e  37458  cdleme20m  37474  cdleme21a  37476  cdleme21b  37477  cdleme21c  37478  cdleme22f2  37498  cdleme28b  37522  cdleme36a  37611  cdleme36m  37612  cdleme41sn4aw  37626  cdleme43bN  37641  cdleme43dN  37643  cdleme46f2g2  37644  cdleme46f2g1  37645  cdleme4gfv  37658  cdlemeg46nlpq  37668  cdlemeg46req  37680  cdlemeg46fgN  37685  cdlemf1  37712  cdlemg8b  37779  cdlemg9a  37783  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg17pq  37823  cdlemg18a  37829  cdlemg18c  37831  cdlemg19a  37834  cdlemg19  37835  cdlemg21  37837  cdlemg31b0N  37845  cdlemg31b0a  37846  cdlemg31c  37850  cdlemg33b0  37852  cdlemg33c0  37853  trlcone  37879  cdlemg42  37880  cdlemg44a  37882  cdlemg46  37886  cdlemh1  37966  cdlemh2  37967  cdlemh  37968  cdlemj3  37974  cdlemk3  37984  cdlemki  37992  cdlemksv2  37998  cdlemk12  38001  cdlemk14  38005  cdlemk15  38006  cdlemk7u  38021  cdlemk11u  38022  cdlemk12u  38023  cdlemk21N  38024  cdlemk20  38025  cdlemk22  38044  cdlemk26-3  38057  cdlemk27-3  38058  cdlemk28-3  38059  cdlemkfid3N  38076  cdlemk11ta  38080  cdlemk47  38100  cdlemk54  38109  dia2dimlem1  38215  dochsat  38534  dochshpncl  38535  lclkrlem2b  38659  lcfrlem21  38714  baerlem5amN  38867  baerlem5bmN  38868  baerlem5abmN  38869  mapdindp4  38874  mapdheq2  38880  mapdheq2biN  38881  mapdh6aN  38886  mapdh6dN  38890  mapdh6eN  38891  mapdh6hN  38894  mapdh7eN  38899  mapdh7dN  38901  mapdh7fN  38902  mapdh8ab  38928  mapdh8ad  38930  mapdh8e  38935  mapdh9a  38940  mapdh9aOLDN  38941  hdmap1l6a  38960  hdmap1l6d  38964  hdmap1l6e  38965  hdmap1l6h  38968  hdmap1eulem  38973  hdmap1eulemOLDN  38974  hdmapval0  38984  hdmapeveclem  38985  hdmapval3lemN  38988  hdmap10lem  38990  hdmap11lem1  38992  hdmaprnlem3N  39001  hdmaprnlem9N  39008  hdmaprnlem3eN  39009  xppss12  39164  jm2.26lem3  39647  rpnnen3lem  39677  rpnnen3  39678  imo72b2lem0  40565  imo72b2lem2  40567  imo72b2  40574  mnuprdlem1  40657  bcc0  40721  chordthmALT  41316  fnchoice  41335  refsum2cnlem1  41343  xrleneltd  41640  xrltned  41674  infleinf  41689  reclt0  41712  icoiccdif  41849  ressiooinf  41882  limcresiooub  41972  limcleqr  41974  limclner  41981  climxrre  42080  icccncfext  42219  cncfiooiccre  42227  dvnxpaek  42276  stoweidlem43  42377  stirlinglem5  42412  stirlinglem7  42414  dirkercncflem1  42437  fourierdlem24  42465  fourierdlem32  42473  fourierdlem33  42474  fourierdlem34  42475  fourierdlem35  42476  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem76  42516  fourierdlem79  42519  fourierdlem81  42521  fourierdlem91  42531  fourierdlem102  42542  fourierdlem114  42554  etransclem15  42583  etransclem24  42592  sge0rpcpnf  42752  sge0isum  42758  pimrecltpos  43036  pimiooltgt  43038  setsnidel  43586  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  fmtnoprmfac2  43778  lighneallem1  43819  lighneallem3  43821  perfectALTVlem2  43936  nnsgrpnmnd  44134  nrhmzr  44193  lvecpsslmod  44611  affinecomb1  44738  affinecomb2  44739  1subrec1sub  44741  rrx2plord2  44758  line  44768  rrxline  44770  eenglngeehlnmlem2  44774  rrx2vlinest  44777  line2xlem  44789  2itscp  44817