Theorem necomd 2997

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

Syntax hints:   → wi 4   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  difsnb  4805  0nelop  5492  xpdifid  6159  difsnen  9041  fofinf1o  9315  en2eleq  9990  en2other2  9991  ackbij1lem15  10216  infpssrlem5  10289  fin23lem24  10304  fin23lem31  10325  isf32lem9  10343  canthnumlem  10630  canthp1lem2  10635  npomex  10978  ltned  11337  lt0ne0  11667  recgt0  12047  zneo  12632  xrltne  13129  supxrbnd  13294  flltnz  13763  seqf1olem1  13994  nn0opthi  14217  hashtpg  14433  hashge3el3dif  14434  cats1un  14658  sumtp  15682  geoserg  15799  geolim  15803  geolim2  15804  tanadd  16097  ruclem6  16165  ruclem7  16166  isprm2lem  16605  isprm5  16631  oddprm  16730  pcmpt  16812  cshwshashlem3  17018  resshom  17351  ressco  17352  mrissmrcd  17571  rescco  17767  estrres  18078  smndex2dnrinv  18783  pmtrprfv  19305  symggen  19322  dprdcntz  19861  dprdres  19881  ablfac1b  19923  01eq0ringOLD  20284  lbspss  20670  lspsnnecom  20709  lspindp2l  20724  lspindp2  20725  islbs3  20745  lbsextlem4  20751  sralemOLD  20768  lidlnz  20829  uvcf1  21320  frlmup2  21327  psrridm  21495  coe1tmfv2  21768  coe1tmmul  21770  dmatmul  21968  mdetralt  22079  mdetunilem2  22084  mdetunilem6  22088  mdetunilem7  22089  maducoeval2  22111  madurid  22115  fvmptnn04ifa  22321  en2top  22457  cmpfi  22881  snfil  23337  tsmsfbas  23601  zcld  24298  iccpnfhmeo  24430  xrhmeo  24431  evth  24444  minveclem3b  24914  i1fres  25192  dvcnvlem  25462  ig1peu  25658  ig1pdvds  25663  aaliou3lem9  25832  taylthlem2  25855  abelthlem2  25913  abelthlem7  25919  cos02pilt1  26004  tanregt0  26017  logcj  26083  argimgt0  26089  dvloglem  26125  logf1o2  26127  logbrec  26254  ang180lem1  26281  ang180lem2  26282  ang180lem3  26283  ang180lem4  26284  ang180lem5  26285  ang180  26286  isosctrlem3  26292  ssscongptld  26294  affineequivne  26299  angpieqvdlem  26300  angpieqvdlem2  26301  angpieqvd  26303  chordthmlem  26304  chordthmlem2  26305  chordthm  26309  asinneg  26358  ppiltx  26648  perfectlem2  26700  lgsneg  26791  lgsqr  26821  lgseisenlem4  26848  lgsquadlem1  26850  lgsquadlem3  26852  lgsquad2  26856  2lgsoddprm  26886  dchrisum0flblem1  26978  noseponlem  27134  nosep1o  27151  nosep2o  27152  nosupbnd2lem1  27185  noinfbnd2lem1  27200  noetasuplem4  27206  noetainflem4  27210  slerec  27287  0elright  27371  tgbtwnouttr  27715  tgifscgr  27726  tgcgrxfr  27736  tglngval  27769  tgfscgr  27786  tgbtwnconn1lem3  27792  tgbtwnconn3  27795  legtrid  27809  hltr  27828  hlbtwn  27829  btwnhl1  27830  btwnhl  27832  hlcgrex  27834  hlcgreulem  27835  lncom  27840  tgisline  27845  tglineeltr  27849  tglineelsb2  27850  tglinecom  27853  tglinethru  27854  ncolncol  27864  coltr  27865  coltr3  27866  symquadlem  27907  midexlem  27910  ragcol  27917  ragcgr  27925  perpneq  27932  footexALT  27936  footexlem1  27937  footexlem2  27938  foot  27940  footne  27941  colperpexlem3  27950  mideulem2  27952  opphllem  27953  midex  27955  opphllem1  27965  opphllem2  27966  opphllem3  27967  opphllem4  27968  opphllem5  27969  opphllem6  27970  outpasch  27973  hlpasch  27974  lnopp2hpgb  27981  colhp  27988  lmieu  28002  hypcgrlem1  28017  hypcgrlem2  28018  lnperpex  28021  trgcopy  28022  trgcopyeulem  28023  iscgra1  28028  cgrane2  28031  cgrane3  28032  cgrane4  28033  cgracgr  28036  cgraid  28037  cgraswap  28038  cgrcgra  28039  cgracom  28040  cgratr  28041  flatcgra  28042  cgraswaplr  28043  cgracol  28046  dfcgra2  28048  sacgr  28049  oacgr  28050  acopy  28051  acopyeu  28052  leagne2  28068  leagne3  28069  cgrg3col4  28071  tgsas1  28072  tgsas2  28074  tgasa1  28076  ttgcontlem1  28109  cchhllemOLD  28112  brbtwn2  28130  axlowdimlem15  28181  axlowdimlem16  28182  axcontlem8  28196  upgrex  28319  edglnl  28370  umgrvad2edg  28437  nbupgr  28568  nbumgrvtx  28570  nbgr2vtx1edg  28574  nbuhgr2vtx1edgb  28576  nbupgrres  28588  cplgr3v  28659  cusgrexilem2  28666  usgredgsscusgredg  28683  1hegrvtxdg1r  28732  1egrvtxdg1r  28734  1egrvtxdg0  28735  pthdadjvtx  28954  pthdlem2lem  28991  wspniunwspnon  29144  umgr2cwwk2dif  29284  3pthdlem1  29384  uhgr3cyclex  29402  upgr4cycl4dv4e  29405  frgr3v  29495  1to3vfriswmgr  29500  frgrwopreglem5a  29531  frgrwopreglem3  29534  frgrhash2wsp  29552  staddi  31464  unidifsnne  31739  ifnefals  31746  coprprop  31892  pmtrcnel  32221  pmtrcnel2  32222  psgnfzto1stlem  32230  cycpmco2lem1  32256  cycpmco2  32263  cyc2fvx  32264  cyc3co2  32270  cycpmrn  32273  tocyccntz  32274  cyc3evpm  32280  cyc3genpmlem  32281  ornglmullt  32387  orngrmullt  32388  orngmullt  32389  ofldlt1  32393  ofldchr  32394  isarchiofld  32397  drngidlhash  32503  qsidomlem2  32523  mxidlnzr  32534  qsdrng  32557  1smat1  32715  submateqlem1  32718  madjusmdetlem2  32739  ordtconnlem1  32835  esumrnmpt2  32997  cntnevol  33157  signstfveq0a  33518  repr0  33554  reprlt  33562  reprinfz1  33565  cusgredgex  34043  2cycl2d  34061  acycgr1v  34071  derangenlem  34093  subfacp1lem1  34101  subfacp1lem3  34104  subfacp1lem5  34106  fmlasucdisj  34321  dfrdg4  34854  ifscgr  34947  cgrxfr  34958  btwnconn1lem8  34997  btwnconn3  35006  segcon2  35008  broutsideof3  35029  outsideoftr  35032  outsideofeq  35033  outsideofeu  35034  lineunray  35050  lineelsb2  35051  linethru  35056  unbdqndv2lem2  35291  knoppndvlem1  35293  knoppndvlem2  35294  knoppndvlem7  35299  knoppndvlem14  35306  bj-bary1lem  36096  bj-bary1lem1  36097  bj-bary1  36098  finxpreclem2  36176  finxp1o  36178  finxpreclem6  36182  fin2solem  36379  poimirlem9  36402  poimirlem15  36408  poimirlem20  36413  poimirlem24  36417  poimirlem25  36418  poimirlem27  36420  itg2addnclem2  36445  ftc1cnnc  36465  heibor1lem  36583  maxidln0  36819  lshpnelb  37760  lsatssn0  37778  lsatcv0  37807  lsat0cv  37809  lsatexch1  37822  l1cvat  37831  atlen0  38086  cvlsupr2  38119  atcvrj2b  38209  2atlt  38216  atbtwn  38223  3noncolr2  38226  4noncolr3  38230  3dimlem3  38238  3dimlem3OLDN  38239  3dimlem4  38241  3dimlem4OLDN  38242  3dim2  38245  1cvratex  38250  1cvrat  38253  ps-1  38254  ps-2  38255  hlatexch4  38258  3atlem4  38263  3atlem6  38265  4atlem0ae  38371  4atlem0be  38372  dalemccnedd  38464  dalemrotps  38468  dalem21  38471  dalem23  38473  dalem27  38476  dalem41  38490  dalem44  38493  dalem54  38503  lnatexN  38556  lnjatN  38557  llnexchb2lem  38645  llnexchb2  38646  lhpn0  38781  lhpexle3lem  38788  lhpmatb  38808  4atexlemswapqr  38840  4atexlemc  38846  4atexlemnclw  38847  4atexlemcnd  38849  4atexlemex4  38850  4atexlemex6  38851  4atex  38853  trlat  38946  trlval4  38965  cdlemc5  38972  cdlemd4  38978  cdlemd7  38981  cdlemd9  38983  cdleme0e  38994  cdleme3b  39006  cdleme3c  39007  cdleme3e  39009  cdleme3h  39012  cdleme7aa  39019  cdleme7e  39024  cdleme7ga  39025  cdleme9  39030  cdleme11c  39038  cdleme11e  39040  cdleme11fN  39041  cdleme11h  39043  cdleme11j  39044  cdleme11k  39045  cdleme15b  39052  cdleme15c  39053  cdleme17c  39065  cdleme18b  39069  cdlemesner  39073  cdleme20zN  39078  cdleme19c  39082  cdleme19d  39083  cdleme19e  39084  cdleme20m  39100  cdleme21a  39102  cdleme21b  39103  cdleme21c  39104  cdleme22f2  39124  cdleme28b  39148  cdleme36a  39237  cdleme36m  39238  cdleme41sn4aw  39252  cdleme43bN  39267  cdleme43dN  39269  cdleme46f2g2  39270  cdleme46f2g1  39271  cdleme4gfv  39284  cdlemeg46nlpq  39294  cdlemeg46req  39306  cdlemeg46fgN  39311  cdlemf1  39338  cdlemg8b  39405  cdlemg9a  39409  cdlemg12g  39426  cdlemg12  39427  cdlemg13a  39428  cdlemg17pq  39449  cdlemg18a  39455  cdlemg18c  39457  cdlemg19a  39460  cdlemg19  39461  cdlemg21  39463  cdlemg31b0N  39471  cdlemg31b0a  39472  cdlemg31c  39476  cdlemg33b0  39478  cdlemg33c0  39479  trlcone  39505  cdlemg42  39506  cdlemg44a  39508  cdlemg46  39512  cdlemh1  39592  cdlemh2  39593  cdlemh  39594  cdlemj3  39600  cdlemk3  39610  cdlemki  39618  cdlemksv2  39624  cdlemk12  39627  cdlemk14  39631  cdlemk15  39632  cdlemk7u  39647  cdlemk11u  39648  cdlemk12u  39649  cdlemk21N  39650  cdlemk20  39651  cdlemk22  39670  cdlemk26-3  39683  cdlemk27-3  39684  cdlemk28-3  39685  cdlemkfid3N  39702  cdlemk11ta  39706  cdlemk47  39726  cdlemk54  39735  dia2dimlem1  39841  dochsat  40160  dochshpncl  40161  lclkrlem2b  40285  lcfrlem21  40340  baerlem5amN  40493  baerlem5bmN  40494  baerlem5abmN  40495  mapdindp4  40500  mapdheq2  40506  mapdheq2biN  40507  mapdh6aN  40512  mapdh6dN  40516  mapdh6eN  40517  mapdh6hN  40520  mapdh7eN  40525  mapdh7dN  40527  mapdh7fN  40528  mapdh8ab  40554  mapdh8ad  40556  mapdh8e  40561  mapdh9a  40566  mapdh9aOLDN  40567  hdmap1l6a  40586  hdmap1l6d  40590  hdmap1l6e  40591  hdmap1l6h  40594  hdmap1eulem  40599  hdmap1eulemOLDN  40600  hdmapval0  40610  hdmapeveclem  40611  hdmapval3lemN  40614  hdmap10lem  40616  hdmap11lem1  40618  hdmaprnlem3N  40627  hdmaprnlem9N  40634  hdmaprnlem3eN  40635  fzne2d  40752  lcmineqlem11  40810  3lexlogpow5ineq1  40825  3lexlogpow5ineq2  40826  3lexlogpow5ineq4  40827  3lexlogpow5ineq3  40828  3lexlogpow2ineq1  40829  3lexlogpow2ineq2  40830  3lexlogpow5ineq5  40831  aks4d1lem1  40833  dvrelog2b  40837  dvrelogpow2b  40839  aks4d1p1p3  40840  aks4d1p1p2  40841  aks4d1p1p4  40842  aks4d1p1p6  40844  aks4d1p1p7  40845  aks4d1p1p5  40846  aks4d1p1  40847  aks4d1p2  40848  aks4d1p3  40849  aks4d1p5  40851  aks4d1p6  40852  aks4d1p7d1  40853  aks4d1p7  40854  aks4d1p8d3  40857  aks4d1p8  40858  aks4d1p9  40859  fldhmf1  40861  aks6d1c2p2  40863  2np3bcnp1  40866  2ap1caineq  40867  sticksstones1  40868  sticksstones2  40869  sticksstones10  40877  sticksstones12a  40879  sticksstones12  40880  sticksstones22  40890  metakunt7  40897  metakunt12  40902  metakunt22  40912  xppss12  40963  mhpind  41055  jm2.26lem3  41611  rpnnen3lem  41641  rpnnen3  41642  imo72b2lem0  42788  imo72b2lem2  42790  imo72b2  42795  mnuprdlem1  42902  bcc0  42970  chordthmALT  43565  fnchoice  43584  refsum2cnlem1  43592  xrleneltd  43906  xrltned  43940  infleinf  43955  reclt0  43974  icoiccdif  44110  ressiooinf  44143  limcresiooub  44231  limcleqr  44233  limclner  44240  climxrre  44339  icccncfext  44476  cncfiooiccre  44484  dvnxpaek  44531  stoweidlem43  44632  stirlinglem5  44667  stirlinglem7  44669  dirkercncflem1  44692  fourierdlem24  44720  fourierdlem32  44728  fourierdlem33  44729  fourierdlem34  44730  fourierdlem35  44731  fourierdlem46  44741  fourierdlem48  44743  fourierdlem49  44744  fourierdlem64  44759  fourierdlem65  44760  fourierdlem74  44769  fourierdlem76  44771  fourierdlem79  44774  fourierdlem81  44776  fourierdlem91  44786  fourierdlem102  44797  fourierdlem114  44809  etransclem15  44838  etransclem24  44847  sge0rpcpnf  45010  sge0isum  45016  pimrecltpos  45297  pimiooltgt  45299  setsnidel  45918  odz2prm2pw  46104  fmtnoprmfac1lem  46105  fmtnoprmfac1  46106  fmtnoprmfac2  46108  lighneallem1  46146  lighneallem3  46148  perfectALTVlem2  46263  nnsgrpnmnd  46461  nrhmzr  46520  lvecpsslmod  47028  affinecomb1  47228  affinecomb2  47229  1subrec1sub  47231  rrx2plord2  47248  line  47258  rrxline  47260  eenglngeehlnmlem2  47264  rrx2vlinest  47267  line2xlem  47279  2itscp  47307