Theorem necomd 2990

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 2988	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)
3	1, 2	sylib 221	1 ⊢ (𝜑 → 𝐵 ≠ 𝐴)

Syntax hints:   → wi 4   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2731  df-ne 2936

This theorem is referenced by:  difsnb  4704  0nelop  5363  xpdifid  6010  difsnen  8660  fofinf1o  8884  en2eleq  9520  en2other2  9521  ackbij1lem15  9746  infpssrlem5  9819  fin23lem24  9834  fin23lem31  9855  isf32lem9  9873  canthnumlem  10160  canthp1lem2  10165  npomex  10508  ltned  10866  lt0ne0  11196  recgt0  11576  zneo  12158  xrltne  12651  supxrbnd  12816  flltnz  13284  seqf1olem1  13513  nn0opthi  13734  hashtpg  13949  hashge3el3dif  13950  cats1un  14184  sumtp  15209  geoserg  15326  geolim  15330  geolim2  15331  tanadd  15624  ruclem6  15692  ruclem7  15693  isprm2lem  16134  isprm5  16160  oddprm  16259  pcmpt  16340  cshwshashlem3  16546  mrissmrcd  17026  estrres  17517  smndex2dnrinv  18208  pmtrprfv  18711  symggen  18728  dprdcntz  19261  dprdres  19281  ablfac1b  19323  lbspss  19985  lspsnnecom  20022  lspindp2l  20037  lspindp2  20038  islbs3  20058  lbsextlem4  20064  sralem  20080  lidlnz  20132  01eq0ring  20176  uvcf1  20620  frlmup2  20627  psrridm  20795  coe1tmfv2  21062  coe1tmmul  21064  dmatmul  21260  mdetralt  21371  mdetunilem2  21376  mdetunilem6  21380  mdetunilem7  21381  maducoeval2  21403  madurid  21407  fvmptnn04ifa  21613  en2top  21748  cmpfi  22171  snfil  22627  tsmsfbas  22891  zcld  23577  iccpnfhmeo  23709  xrhmeo  23710  evth  23723  minveclem3b  24192  i1fres  24470  dvcnvlem  24740  ig1peu  24936  ig1pdvds  24941  aaliou3lem9  25110  taylthlem2  25133  abelthlem2  25191  abelthlem7  25197  cos02pilt1  25282  tanregt0  25295  logcj  25361  argimgt0  25367  dvloglem  25403  logf1o2  25405  logbrec  25532  ang180lem1  25559  ang180lem2  25560  ang180lem3  25561  ang180lem4  25562  ang180lem5  25563  ang180  25564  isosctrlem3  25570  ssscongptld  25572  affineequivne  25577  angpieqvdlem  25578  angpieqvdlem2  25579  angpieqvd  25581  chordthmlem  25582  chordthmlem2  25583  chordthm  25587  asinneg  25636  ppiltx  25926  perfectlem2  25978  lgsneg  26069  lgsqr  26099  lgseisenlem4  26126  lgsquadlem1  26128  lgsquadlem3  26130  lgsquad2  26134  2lgsoddprm  26164  dchrisum0flblem1  26256  tgbtwnouttr  26455  tgifscgr  26466  tgcgrxfr  26476  tglngval  26509  tgfscgr  26526  tgbtwnconn1lem3  26532  tgbtwnconn3  26535  legtrid  26549  hltr  26568  hlbtwn  26569  btwnhl1  26570  btwnhl  26572  hlcgrex  26574  hlcgreulem  26575  lncom  26580  tgisline  26585  tglineeltr  26589  tglineelsb2  26590  tglinecom  26593  tglinethru  26594  ncolncol  26604  coltr  26605  coltr3  26606  symquadlem  26647  midexlem  26650  ragcol  26657  ragcgr  26665  perpneq  26672  footexALT  26676  footexlem1  26677  footexlem2  26678  foot  26680  footne  26681  colperpexlem3  26690  mideulem2  26692  opphllem  26693  midex  26695  opphllem1  26705  opphllem2  26706  opphllem3  26707  opphllem4  26708  opphllem5  26709  opphllem6  26710  outpasch  26713  hlpasch  26714  lnopp2hpgb  26721  colhp  26728  lmieu  26742  hypcgrlem1  26757  hypcgrlem2  26758  lnperpex  26761  trgcopy  26762  trgcopyeulem  26763  iscgra1  26768  cgrane2  26771  cgrane3  26772  cgrane4  26773  cgracgr  26776  cgraid  26777  cgraswap  26778  cgrcgra  26779  cgracom  26780  cgratr  26781  flatcgra  26782  cgraswaplr  26783  cgracol  26786  dfcgra2  26788  sacgr  26789  oacgr  26790  acopy  26791  acopyeu  26792  leagne2  26808  leagne3  26809  cgrg3col4  26811  tgsas1  26812  tgsas2  26814  tgasa1  26816  ttgcontlem1  26843  cchhllem  26845  brbtwn2  26863  axlowdimlem15  26914  axlowdimlem16  26915  axcontlem8  26929  upgrex  27049  edglnl  27100  umgrvad2edg  27167  nbupgr  27298  nbumgrvtx  27300  nbgr2vtx1edg  27304  nbuhgr2vtx1edgb  27306  nbupgrres  27318  cplgr3v  27389  cusgrexilem2  27396  usgredgsscusgredg  27413  1hegrvtxdg1r  27462  1egrvtxdg1r  27464  1egrvtxdg0  27465  pthdadjvtx  27683  pthdlem2lem  27720  wspniunwspnon  27873  umgr2cwwk2dif  28013  3pthdlem1  28113  uhgr3cyclex  28131  upgr4cycl4dv4e  28134  frgr3v  28224  1to3vfriswmgr  28229  frgrwopreglem5a  28260  frgrwopreglem3  28263  frgrhash2wsp  28281  staddi  30193  unidifsnne  30470  coprprop  30619  pmtrcnel  30947  pmtrcnel2  30948  psgnfzto1stlem  30956  cycpmco2lem1  30982  cycpmco2  30989  cyc2fvx  30990  cyc3co2  30996  cycpmrn  30999  tocyccntz  31000  cyc3evpm  31006  cyc3genpmlem  31007  ornglmullt  31095  orngrmullt  31096  orngmullt  31097  ofldlt1  31101  ofldchr  31102  isarchiofld  31105  qsidomlem2  31213  mxidlnzr  31223  1smat1  31338  submateqlem1  31341  madjusmdetlem2  31362  ordtconnlem1  31458  esumrnmpt2  31618  cntnevol  31778  signstfveq0a  32137  repr0  32173  reprlt  32181  reprinfz1  32184  cusgredgex  32666  2cycl2d  32684  acycgr1v  32694  derangenlem  32716  subfacp1lem1  32724  subfacp1lem3  32727  subfacp1lem5  32729  fmlasucdisj  32944  noseponlem  33522  nosep1o  33539  nosep2o  33540  nosupbnd2lem1  33573  noinfbnd2lem1  33588  noetasuplem4  33594  noetainflem4  33598  slerec  33668  dfrdg4  33908  ifscgr  34001  cgrxfr  34012  btwnconn1lem8  34051  btwnconn3  34060  segcon2  34062  broutsideof3  34083  outsideoftr  34086  outsideofeq  34087  outsideofeu  34088  lineunray  34104  lineelsb2  34105  linethru  34110  unbdqndv2lem2  34345  knoppndvlem1  34347  knoppndvlem2  34348  knoppndvlem7  34353  knoppndvlem14  34360  bj-bary1lem  35133  bj-bary1lem1  35134  bj-bary1  35135  finxpreclem2  35216  finxp1o  35218  finxpreclem6  35222  fin2solem  35418  poimirlem9  35441  poimirlem15  35447  poimirlem20  35452  poimirlem24  35456  poimirlem25  35457  poimirlem27  35459  itg2addnclem2  35484  ftc1cnnc  35504  heibor1lem  35622  maxidln0  35858  lshpnelb  36653  lsatssn0  36671  lsatcv0  36700  lsat0cv  36702  lsatexch1  36715  l1cvat  36724  atlen0  36979  cvlsupr2  37012  atcvrj2b  37101  2atlt  37108  atbtwn  37115  3noncolr2  37118  4noncolr3  37122  3dimlem3  37130  3dimlem3OLDN  37131  3dimlem4  37133  3dimlem4OLDN  37134  3dim2  37137  1cvratex  37142  1cvrat  37145  ps-1  37146  ps-2  37147  hlatexch4  37150  3atlem4  37155  3atlem6  37157  4atlem0ae  37263  4atlem0be  37264  dalemccnedd  37356  dalemrotps  37360  dalem21  37363  dalem23  37365  dalem27  37368  dalem41  37382  dalem44  37385  dalem54  37395  lnatexN  37448  lnjatN  37449  llnexchb2lem  37537  llnexchb2  37538  lhpn0  37673  lhpexle3lem  37680  lhpmatb  37700  4atexlemswapqr  37732  4atexlemc  37738  4atexlemnclw  37739  4atexlemcnd  37741  4atexlemex4  37742  4atexlemex6  37743  4atex  37745  trlat  37838  trlval4  37857  cdlemc5  37864  cdlemd4  37870  cdlemd7  37873  cdlemd9  37875  cdleme0e  37886  cdleme3b  37898  cdleme3c  37899  cdleme3e  37901  cdleme3h  37904  cdleme7aa  37911  cdleme7e  37916  cdleme7ga  37917  cdleme9  37922  cdleme11c  37930  cdleme11e  37932  cdleme11fN  37933  cdleme11h  37935  cdleme11j  37936  cdleme11k  37937  cdleme15b  37944  cdleme15c  37945  cdleme17c  37957  cdleme18b  37961  cdlemesner  37965  cdleme20zN  37970  cdleme19c  37974  cdleme19d  37975  cdleme19e  37976  cdleme20m  37992  cdleme21a  37994  cdleme21b  37995  cdleme21c  37996  cdleme22f2  38016  cdleme28b  38040  cdleme36a  38129  cdleme36m  38130  cdleme41sn4aw  38144  cdleme43bN  38159  cdleme43dN  38161  cdleme46f2g2  38162  cdleme46f2g1  38163  cdleme4gfv  38176  cdlemeg46nlpq  38186  cdlemeg46req  38198  cdlemeg46fgN  38203  cdlemf1  38230  cdlemg8b  38297  cdlemg9a  38301  cdlemg12g  38318  cdlemg12  38319  cdlemg13a  38320  cdlemg17pq  38341  cdlemg18a  38347  cdlemg18c  38349  cdlemg19a  38352  cdlemg19  38353  cdlemg21  38355  cdlemg31b0N  38363  cdlemg31b0a  38364  cdlemg31c  38368  cdlemg33b0  38370  cdlemg33c0  38371  trlcone  38397  cdlemg42  38398  cdlemg44a  38400  cdlemg46  38404  cdlemh1  38484  cdlemh2  38485  cdlemh  38486  cdlemj3  38492  cdlemk3  38502  cdlemki  38510  cdlemksv2  38516  cdlemk12  38519  cdlemk14  38523  cdlemk15  38524  cdlemk7u  38539  cdlemk11u  38540  cdlemk12u  38541  cdlemk21N  38542  cdlemk20  38543  cdlemk22  38562  cdlemk26-3  38575  cdlemk27-3  38576  cdlemk28-3  38577  cdlemkfid3N  38594  cdlemk11ta  38598  cdlemk47  38618  cdlemk54  38627  dia2dimlem1  38733  dochsat  39052  dochshpncl  39053  lclkrlem2b  39177  lcfrlem21  39232  baerlem5amN  39385  baerlem5bmN  39386  baerlem5abmN  39387  mapdindp4  39392  mapdheq2  39398  mapdheq2biN  39399  mapdh6aN  39404  mapdh6dN  39408  mapdh6eN  39409  mapdh6hN  39412  mapdh7eN  39417  mapdh7dN  39419  mapdh7fN  39420  mapdh8ab  39446  mapdh8ad  39448  mapdh8e  39453  mapdh9a  39458  mapdh9aOLDN  39459  hdmap1l6a  39478  hdmap1l6d  39482  hdmap1l6e  39483  hdmap1l6h  39486  hdmap1eulem  39491  hdmap1eulemOLDN  39492  hdmapval0  39502  hdmapeveclem  39503  hdmapval3lemN  39506  hdmap10lem  39508  hdmap11lem1  39510  hdmaprnlem3N  39519  hdmaprnlem9N  39526  hdmaprnlem3eN  39527  fzne2d  39641  lcmineqlem11  39699  3lexlogpow5ineq1  39714  3lexlogpow5ineq2  39715  3lexlogpow5ineq4  39716  3lexlogpow5ineq3  39717  3lexlogpow2ineq1  39718  3lexlogpow2ineq2  39719  3lexlogpow5ineq5  39720  dvrelog2b  39725  dvrelogpow2b  39727  aks4d1p1p3  39728  aks4d1p1p2  39729  aks4d1p1p4  39730  aks4d1p1p6  39732  aks4d1p1p7  39733  aks4d1p1p5  39734  aks4d1p1  39735  2np3bcnp1  39738  2ap1caineq  39739  sticksstones1  39740  sticksstones2  39741  sticksstones10  39749  sticksstones12a  39751  sticksstones12  39752  metakunt7  39762  metakunt12  39767  metakunt22  39777  xppss12  39826  mhpind  39902  jm2.26lem3  40435  rpnnen3lem  40465  rpnnen3  40466  imo72b2lem0  41362  imo72b2lem2  41364  imo72b2  41370  mnuprdlem1  41472  bcc0  41536  chordthmALT  42131  fnchoice  42150  refsum2cnlem1  42158  xrleneltd  42440  xrltned  42474  infleinf  42489  reclt0  42509  icoiccdif  42642  ressiooinf  42675  limcresiooub  42765  limcleqr  42767  limclner  42774  climxrre  42873  icccncfext  43010  cncfiooiccre  43018  dvnxpaek  43065  stoweidlem43  43166  stirlinglem5  43201  stirlinglem7  43203  dirkercncflem1  43226  fourierdlem24  43254  fourierdlem32  43262  fourierdlem33  43263  fourierdlem34  43264  fourierdlem35  43265  fourierdlem46  43275  fourierdlem48  43277  fourierdlem49  43278  fourierdlem64  43293  fourierdlem65  43294  fourierdlem74  43303  fourierdlem76  43305  fourierdlem79  43308  fourierdlem81  43310  fourierdlem91  43320  fourierdlem102  43331  fourierdlem114  43343  etransclem15  43372  etransclem24  43381  sge0rpcpnf  43541  sge0isum  43547  pimrecltpos  43825  pimiooltgt  43827  setsnidel  44410  odz2prm2pw  44596  fmtnoprmfac1lem  44597  fmtnoprmfac1  44598  fmtnoprmfac2  44600  lighneallem1  44638  lighneallem3  44640  perfectALTVlem2  44755  nnsgrpnmnd  44953  nrhmzr  45012  lvecpsslmod  45429  affinecomb1  45629  affinecomb2  45630  1subrec1sub  45632  rrx2plord2  45649  line  45659  rrxline  45661  eenglngeehlnmlem2  45665  rrx2vlinest  45668  line2xlem  45680  2itscp  45708