Theorem necomd 2837

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

Syntax hints:   → wi 4   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  difsnb  4278  0nelop  4886  xpdifid  5481  difsnen  7927  fofinf1o  8126  en2eleq  8714  en2other2  8715  ackbij1lem15  8939  infpssrlem5  9012  fin23lem24  9027  fin23lem31  9048  isf32lem9  9066  canthnumlem  9349  canthp1lem2  9354  npomex  9697  ltned  10052  lt0ne0  10373  recgt0  10746  zneo  11336  xrltne  11870  supxrbnd  12030  flltnz  12474  seqf1olem1  12702  nn0opthi  12919  hashtpg  13121  hashge3el3dif  13122  cats1un  13327  sumtp  14322  geoserg  14437  geolim  14440  geolim2  14441  tanadd  14736  ruclem6  14803  ruclem7  14804  isprm5  15257  oddprm  15353  pcmpt  15434  cshwshashlem3  15642  mrissmrcd  16123  estrres  16602  pmtrprfv  17696  symggen  17713  dprdcntz  18230  dprdres  18250  ablfac1b  18292  lbspss  18903  lspsnnecom  18940  lspindp2l  18955  lspindp2  18956  islbs3  18976  lbsextlem4  18982  sralem  18998  lidlnz  19049  01eq0ring  19093  psrridm  19225  coe1tmfv2  19466  coe1tmmul  19468  uvcf1  19950  frlmup2  19957  dmatmul  20122  mdetralt  20233  mdetunilem2  20238  mdetunilem6  20242  mdetunilem7  20243  maducoeval2  20265  madurid  20269  fvmptnn04ifa  20474  en2top  20600  cmpfi  21021  snfil  21478  tsmsfbas  21741  zcld  22424  iccpnfhmeo  22552  xrhmeo  22553  evth  22566  minveclem3b  23007  i1fres  23278  dvcnvlem  23543  ig1peu  23735  ig1pdvds  23740  aaliou3lem9  23909  taylthlem2  23932  abelthlem2  23990  abelthlem7  23996  tanregt0  24089  logcj  24156  argimgt0  24162  dvloglem  24194  logf1o2  24196  logbrec  24320  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  ang180lem4  24342  ang180lem5  24343  ang180  24344  isosctrlem3  24350  ssscongptld  24352  angpieqvdlem  24355  angpieqvdlem2  24356  angpieqvd  24358  chordthmlem  24359  chordthmlem2  24360  chordthm  24364  asinneg  24413  ppiltx  24703  perfectlem2  24755  lgsneg  24846  lgsqr  24876  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem3  24907  lgsquad2  24911  2lgsoddprm  24941  dchrisum0flblem1  24997  tgbtwnouttr  25192  tgifscgr  25203  tgcgrxfr  25213  tglngval  25246  tgfscgr  25263  tgbtwnconn1lem3  25269  tgbtwnconn3  25272  legtrid  25286  hltr  25305  hlbtwn  25306  btwnhl1  25307  btwnhl  25309  hlcgrex  25311  hlcgreulem  25312  lncom  25317  tgisline  25322  tglineeltr  25326  tglineelsb2  25327  tglinecom  25330  tglinethru  25331  ncolncol  25341  coltr  25342  coltr3  25343  symquadlem  25384  midexlem  25387  ragcol  25394  ragcgr  25402  perpneq  25409  footex  25413  foot  25414  footne  25415  colperpexlem3  25424  mideulem2  25426  opphllem  25427  midex  25429  opphllem1  25439  opphllem2  25440  opphllem3  25441  opphllem4  25442  opphllem5  25443  opphllem6  25444  outpasch  25447  hlpasch  25448  lnopp2hpgb  25455  colhp  25462  lmieu  25476  hypcgrlem1  25491  hypcgrlem2  25492  lnperpex  25495  trgcopy  25496  trgcopyeulem  25497  iscgra1  25502  cgrane2  25505  cgrane3  25506  cgrane4  25507  cgracgr  25510  cgraid  25511  cgraswap  25512  cgrcgra  25513  cgracom  25514  cgratr  25515  cgraswaplr  25516  cgracol  25519  dfcgra2  25521  sacgr  25522  oacgr  25523  acopy  25524  acopyeu  25525  cgrg3col4  25534  tgsas1  25535  tgsas2  25537  tgasa1  25539  tgsss1  25541  isoas  25544  ttgcontlem1  25565  cchhllem  25567  brbtwn2  25585  axlowdimlem15  25636  axlowdimlem16  25637  axcontlem8  25651  structvtxvallem  25697  upgrex  25759  umgraex  25852  isusgra0  25876  usgraop  25879  usgra1v  25919  cyclnspth  26159  4cycl4dv  26195  usg2cwwk2dif  26348  2spot2iun2spont  26418  vdgr1a  26433  eupap1  26503  eupath2lem3  26506  1to3vfriswmgra  26534  frghash2spot  26590  staddi  28489  ornglmullt  29138  orngrmullt  29139  orngmullt  29140  ofldlt1  29144  ofldchr  29145  isarchiofld  29148  psgnfzto1stlem  29181  1smat1  29198  submateqlem1  29201  madjusmdetlem2  29222  ordtconlem1  29298  esumrnmpt2  29457  cntnevol  29618  signstfveq0a  29979  derangenlem  30407  subfacp1lem1  30415  subfacp1lem3  30418  subfacp1lem5  30420  noseponlem  31065  nodenselem3  31082  dfrdg4  31228  ifscgr  31321  cgrxfr  31332  btwnconn1lem8  31371  btwnconn3  31380  segcon2  31382  broutsideof3  31403  outsideoftr  31406  outsideofeq  31407  outsideofeu  31408  lineunray  31424  lineelsb2  31425  linethru  31430  unbdqndv2lem2  31671  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem14  31686  bj-bary1lem  32337  bj-bary1lem1  32338  bj-bary1  32339  finxpreclem2  32403  finxp1o  32405  finxpreclem6  32409  fin2solem  32565  poimirlem9  32588  poimirlem15  32594  poimirlem20  32599  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  itg2addnclem2  32632  ftc1cnnc  32654  heibor1lem  32778  maxidln0  33014  lshpnelb  33289  lsatssn0  33307  lsatcv0  33336  lsat0cv  33338  lsatexch1  33351  l1cvat  33360  atlen0  33615  cvlsupr2  33648  atcvrj2b  33736  2atlt  33743  atbtwn  33750  3noncolr2  33753  4noncolr3  33757  3dimlem3  33765  3dimlem3OLDN  33766  3dimlem4  33768  3dimlem4OLDN  33769  3dim2  33772  1cvratex  33777  1cvrat  33780  ps-1  33781  ps-2  33782  hlatexch4  33785  3atlem4  33790  3atlem6  33792  4atlem0ae  33898  4atlem0be  33899  dalemccnedd  33991  dalemrotps  33995  dalem21  33998  dalem23  34000  dalem27  34003  dalem41  34017  dalem44  34020  dalem54  34030  lnatexN  34083  lnjatN  34084  llnexchb2lem  34172  llnexchb2  34173  lhpn0  34308  lhpexle3lem  34315  lhpmatb  34335  4atexlemswapqr  34367  4atexlemc  34373  4atexlemnclw  34374  4atexlemcnd  34376  4atexlemex4  34377  4atexlemex6  34378  4atex  34380  trlat  34474  trlval4  34493  cdlemc5  34500  cdlemd4  34506  cdlemd7  34509  cdlemd9  34511  cdleme0e  34522  cdleme3b  34534  cdleme3c  34535  cdleme3e  34537  cdleme3h  34540  cdleme7aa  34547  cdleme7e  34552  cdleme7ga  34553  cdleme9  34558  cdleme11c  34566  cdleme11e  34568  cdleme11fN  34569  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme15b  34580  cdleme15c  34581  cdleme17c  34593  cdleme18b  34597  cdlemesner  34601  cdleme20zN  34606  cdleme19c  34611  cdleme19d  34612  cdleme19e  34613  cdleme20m  34629  cdleme21a  34631  cdleme21b  34632  cdleme21c  34633  cdleme22f2  34653  cdleme28b  34677  cdleme36a  34766  cdleme36m  34767  cdleme41sn4aw  34781  cdleme43bN  34796  cdleme43dN  34798  cdleme46f2g2  34799  cdleme46f2g1  34800  cdleme4gfv  34813  cdlemeg46nlpq  34823  cdlemeg46req  34835  cdlemeg46fgN  34840  cdlemf1  34867  cdlemg8b  34934  cdlemg9a  34938  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg17pq  34978  cdlemg18a  34984  cdlemg18c  34986  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemg31c  35005  cdlemg33b0  35007  cdlemg33c0  35008  trlcone  35034  cdlemg42  35035  cdlemg44a  35037  cdlemg46  35041  cdlemh1  35121  cdlemh2  35122  cdlemh  35123  cdlemj3  35129  cdlemk3  35139  cdlemki  35147  cdlemksv2  35153  cdlemk12  35156  cdlemk14  35160  cdlemk15  35161  cdlemk7u  35176  cdlemk11u  35177  cdlemk12u  35178  cdlemk21N  35179  cdlemk20  35180  cdlemk22  35199  cdlemk26-3  35212  cdlemk27-3  35213  cdlemk28-3  35214  cdlemkfid3N  35231  cdlemk11ta  35235  cdlemk47  35255  cdlemk54  35264  dia2dimlem1  35371  dochsat  35690  dochshpncl  35691  lclkrlem2b  35815  lcfrlem21  35870  baerlem5amN  36023  baerlem5bmN  36024  baerlem5abmN  36025  mapdindp4  36030  mapdheq2  36036  mapdheq2biN  36037  mapdh6aN  36042  mapdh6dN  36046  mapdh6eN  36047  mapdh6hN  36050  mapdh7eN  36055  mapdh7dN  36057  mapdh7fN  36058  mapdh8ab  36084  mapdh8ad  36086  mapdh8e  36091  mapdh9a  36097  mapdh9aOLDN  36098  hdmap1l6a  36117  hdmap1l6d  36121  hdmap1l6e  36122  hdmap1l6h  36125  hdmap1eulem  36131  hdmap1eulemOLDN  36132  hdmapval0  36143  hdmapeveclem  36144  hdmapval3lemN  36147  hdmap10lem  36149  hdmap11lem1  36151  hdmaprnlem3N  36160  hdmaprnlem9N  36167  hdmaprnlem3eN  36168  jm2.26lem3  36586  rpnnen3lem  36616  rpnnen3  36617  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  bcc0  37561  chordthmALT  38191  fnchoice  38211  refsum2cnlem1  38219  xrleneltd  38480  xrltned  38514  infleinf  38529  reclt0  38555  icoiccdif  38597  ressiooinf  38631  limcresiooub  38709  limcleqr  38711  limclner  38718  icccncfext  38773  cncfiooiccre  38781  dvnxpaek  38832  stoweidlem43  38936  stirlinglem5  38971  stirlinglem7  38973  dirkercncflem1  38996  fourierdlem24  39024  fourierdlem32  39032  fourierdlem33  39033  fourierdlem34  39034  fourierdlem35  39035  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem64  39063  fourierdlem65  39064  fourierdlem74  39073  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem91  39090  fourierdlem102  39101  fourierdlem114  39113  etransclem15  39142  etransclem24  39151  sge0rpcpnf  39314  sge0isum  39320  pimrecltpos  39596  pimiooltgt  39598  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnoprmfac2  40017  lighneallem1  40060  lighneallem3  40062  perfectALTVlem2  40165  umgrvad2edg  40440  nbupgr  40566  nbumgrvtx  40568  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nbupgrres  40592  cplgr3v  40657  cusgrexi  40662  usgredgsscusgredg  40675  1hegrvtxdg1r  40724  1egrvtxdg1r  40726  1egrvtxdg0  40727  pthdadjvtx  40936  pthdlem2lem  40973  wspniunwspnon  41130  umgr2cwwk2dif  41248  3pthdlem1  41331  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  frgr3v  41445  1to3vfriswmgr  41450  frgrwopreglem3  41483  frgrhash2wsp  41497  nnsgrpnmnd  41608  nrhmzr  41663  lvecpsslmod  42090