Theorem necomd 2996

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

Syntax hints:   → wi 4   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  difsnb  4809  0nelop  5496  xpdifid  6167  difsnen  9052  fofinf1o  9326  en2eleq  10002  en2other2  10003  ackbij1lem15  10228  infpssrlem5  10301  fin23lem24  10316  fin23lem31  10337  isf32lem9  10355  canthnumlem  10642  canthp1lem2  10647  npomex  10990  ltned  11349  lt0ne0  11679  recgt0  12059  zneo  12644  xrltne  13141  supxrbnd  13306  flltnz  13775  seqf1olem1  14006  nn0opthi  14229  hashtpg  14445  hashge3el3dif  14446  cats1un  14670  sumtp  15694  geoserg  15811  geolim  15815  geolim2  15816  tanadd  16109  ruclem6  16177  ruclem7  16178  isprm2lem  16617  isprm5  16643  oddprm  16742  pcmpt  16824  cshwshashlem3  17030  resshom  17363  ressco  17364  mrissmrcd  17583  rescco  17779  estrres  18090  smndex2dnrinv  18795  pmtrprfv  19320  symggen  19337  dprdcntz  19877  dprdres  19897  ablfac1b  19939  01eq0ringOLD  20305  lbspss  20692  lspsnnecom  20731  lspindp2l  20746  lspindp2  20747  islbs3  20767  lbsextlem4  20773  sralemOLD  20790  lidlnz  20852  uvcf1  21346  frlmup2  21353  psrridm  21523  coe1tmfv2  21796  coe1tmmul  21798  dmatmul  21998  mdetralt  22109  mdetunilem2  22114  mdetunilem6  22118  mdetunilem7  22119  maducoeval2  22141  madurid  22145  fvmptnn04ifa  22351  en2top  22487  cmpfi  22911  snfil  23367  tsmsfbas  23631  zcld  24328  iccpnfhmeo  24460  xrhmeo  24461  evth  24474  minveclem3b  24944  i1fres  25222  dvcnvlem  25492  ig1peu  25688  ig1pdvds  25693  aaliou3lem9  25862  taylthlem2  25885  abelthlem2  25943  abelthlem7  25949  cos02pilt1  26034  tanregt0  26047  logcj  26113  argimgt0  26119  dvloglem  26155  logf1o2  26157  logbrec  26284  ang180lem1  26311  ang180lem2  26312  ang180lem3  26313  ang180lem4  26314  ang180lem5  26315  ang180  26316  isosctrlem3  26322  ssscongptld  26324  affineequivne  26329  angpieqvdlem  26330  angpieqvdlem2  26331  angpieqvd  26333  chordthmlem  26334  chordthmlem2  26335  chordthm  26339  asinneg  26388  ppiltx  26678  perfectlem2  26730  lgsneg  26821  lgsqr  26851  lgseisenlem4  26878  lgsquadlem1  26880  lgsquadlem3  26882  lgsquad2  26886  2lgsoddprm  26916  dchrisum0flblem1  27008  noseponlem  27164  nosep1o  27181  nosep2o  27182  nosupbnd2lem1  27215  noinfbnd2lem1  27230  noetasuplem4  27236  noetainflem4  27240  slerec  27317  0elright  27401  tgbtwnouttr  27745  tgifscgr  27756  tgcgrxfr  27766  tglngval  27799  tgfscgr  27816  tgbtwnconn1lem3  27822  tgbtwnconn3  27825  legtrid  27839  hltr  27858  hlbtwn  27859  btwnhl1  27860  btwnhl  27862  hlcgrex  27864  hlcgreulem  27865  lncom  27870  tgisline  27875  tglineeltr  27879  tglineelsb2  27880  tglinecom  27883  tglinethru  27884  ncolncol  27894  coltr  27895  coltr3  27896  symquadlem  27937  midexlem  27940  ragcol  27947  ragcgr  27955  perpneq  27962  footexALT  27966  footexlem1  27967  footexlem2  27968  foot  27970  footne  27971  colperpexlem3  27980  mideulem2  27982  opphllem  27983  midex  27985  opphllem1  27995  opphllem2  27996  opphllem3  27997  opphllem4  27998  opphllem5  27999  opphllem6  28000  outpasch  28003  hlpasch  28004  lnopp2hpgb  28011  colhp  28018  lmieu  28032  hypcgrlem1  28047  hypcgrlem2  28048  lnperpex  28051  trgcopy  28052  trgcopyeulem  28053  iscgra1  28058  cgrane2  28061  cgrane3  28062  cgrane4  28063  cgracgr  28066  cgraid  28067  cgraswap  28068  cgrcgra  28069  cgracom  28070  cgratr  28071  flatcgra  28072  cgraswaplr  28073  cgracol  28076  dfcgra2  28078  sacgr  28079  oacgr  28080  acopy  28081  acopyeu  28082  leagne2  28098  leagne3  28099  cgrg3col4  28101  tgsas1  28102  tgsas2  28104  tgasa1  28106  ttgcontlem1  28139  cchhllemOLD  28142  brbtwn2  28160  axlowdimlem15  28211  axlowdimlem16  28212  axcontlem8  28226  upgrex  28349  edglnl  28400  umgrvad2edg  28467  nbupgr  28598  nbumgrvtx  28600  nbgr2vtx1edg  28604  nbuhgr2vtx1edgb  28606  nbupgrres  28618  cplgr3v  28689  cusgrexilem2  28696  usgredgsscusgredg  28713  1hegrvtxdg1r  28762  1egrvtxdg1r  28764  1egrvtxdg0  28765  pthdadjvtx  28984  pthdlem2lem  29021  wspniunwspnon  29174  umgr2cwwk2dif  29314  3pthdlem1  29414  uhgr3cyclex  29432  upgr4cycl4dv4e  29435  frgr3v  29525  1to3vfriswmgr  29530  frgrwopreglem5a  29561  frgrwopreglem3  29564  frgrhash2wsp  29582  staddi  31494  unidifsnne  31768  ifnefals  31775  coprprop  31916  pmtrcnel  32245  pmtrcnel2  32246  psgnfzto1stlem  32254  cycpmco2lem1  32280  cycpmco2  32287  cyc2fvx  32288  cyc3co2  32294  cycpmrn  32297  tocyccntz  32298  cyc3evpm  32304  cyc3genpmlem  32305  ornglmullt  32420  orngrmullt  32421  orngmullt  32422  ofldlt1  32426  ofldchr  32427  isarchiofld  32430  drngidlhash  32547  qsidomlem2  32567  mxidlnzr  32578  drng0mxidl  32587  drngmxidl  32588  qsdrng  32606  ply1annnr  32759  1smat1  32779  submateqlem1  32782  madjusmdetlem2  32803  ordtconnlem1  32899  esumrnmpt2  33061  cntnevol  33221  signstfveq0a  33582  repr0  33618  reprlt  33626  reprinfz1  33629  cusgredgex  34107  2cycl2d  34125  acycgr1v  34135  derangenlem  34157  subfacp1lem1  34165  subfacp1lem3  34168  subfacp1lem5  34170  fmlasucdisj  34385  dfrdg4  34918  ifscgr  35011  cgrxfr  35022  btwnconn1lem8  35061  btwnconn3  35070  segcon2  35072  broutsideof3  35093  outsideoftr  35096  outsideofeq  35097  outsideofeu  35098  lineunray  35114  lineelsb2  35115  linethru  35120  unbdqndv2lem2  35381  knoppndvlem1  35383  knoppndvlem2  35384  knoppndvlem7  35389  knoppndvlem14  35396  bj-bary1lem  36186  bj-bary1lem1  36187  bj-bary1  36188  finxpreclem2  36266  finxp1o  36268  finxpreclem6  36272  fin2solem  36469  poimirlem9  36492  poimirlem15  36498  poimirlem20  36503  poimirlem24  36507  poimirlem25  36508  poimirlem27  36510  itg2addnclem2  36535  ftc1cnnc  36555  heibor1lem  36672  maxidln0  36908  lshpnelb  37849  lsatssn0  37867  lsatcv0  37896  lsat0cv  37898  lsatexch1  37911  l1cvat  37920  atlen0  38175  cvlsupr2  38208  atcvrj2b  38298  2atlt  38305  atbtwn  38312  3noncolr2  38315  4noncolr3  38319  3dimlem3  38327  3dimlem3OLDN  38328  3dimlem4  38330  3dimlem4OLDN  38331  3dim2  38334  1cvratex  38339  1cvrat  38342  ps-1  38343  ps-2  38344  hlatexch4  38347  3atlem4  38352  3atlem6  38354  4atlem0ae  38460  4atlem0be  38461  dalemccnedd  38553  dalemrotps  38557  dalem21  38560  dalem23  38562  dalem27  38565  dalem41  38579  dalem44  38582  dalem54  38592  lnatexN  38645  lnjatN  38646  llnexchb2lem  38734  llnexchb2  38735  lhpn0  38870  lhpexle3lem  38877  lhpmatb  38897  4atexlemswapqr  38929  4atexlemc  38935  4atexlemnclw  38936  4atexlemcnd  38938  4atexlemex4  38939  4atexlemex6  38940  4atex  38942  trlat  39035  trlval4  39054  cdlemc5  39061  cdlemd4  39067  cdlemd7  39070  cdlemd9  39072  cdleme0e  39083  cdleme3b  39095  cdleme3c  39096  cdleme3e  39098  cdleme3h  39101  cdleme7aa  39108  cdleme7e  39113  cdleme7ga  39114  cdleme9  39119  cdleme11c  39127  cdleme11e  39129  cdleme11fN  39130  cdleme11h  39132  cdleme11j  39133  cdleme11k  39134  cdleme15b  39141  cdleme15c  39142  cdleme17c  39154  cdleme18b  39158  cdlemesner  39162  cdleme20zN  39167  cdleme19c  39171  cdleme19d  39172  cdleme19e  39173  cdleme20m  39189  cdleme21a  39191  cdleme21b  39192  cdleme21c  39193  cdleme22f2  39213  cdleme28b  39237  cdleme36a  39326  cdleme36m  39327  cdleme41sn4aw  39341  cdleme43bN  39356  cdleme43dN  39358  cdleme46f2g2  39359  cdleme46f2g1  39360  cdleme4gfv  39373  cdlemeg46nlpq  39383  cdlemeg46req  39395  cdlemeg46fgN  39400  cdlemf1  39427  cdlemg8b  39494  cdlemg9a  39498  cdlemg12g  39515  cdlemg12  39516  cdlemg13a  39517  cdlemg17pq  39538  cdlemg18a  39544  cdlemg18c  39546  cdlemg19a  39549  cdlemg19  39550  cdlemg21  39552  cdlemg31b0N  39560  cdlemg31b0a  39561  cdlemg31c  39565  cdlemg33b0  39567  cdlemg33c0  39568  trlcone  39594  cdlemg42  39595  cdlemg44a  39597  cdlemg46  39601  cdlemh1  39681  cdlemh2  39682  cdlemh  39683  cdlemj3  39689  cdlemk3  39699  cdlemki  39707  cdlemksv2  39713  cdlemk12  39716  cdlemk14  39720  cdlemk15  39721  cdlemk7u  39736  cdlemk11u  39737  cdlemk12u  39738  cdlemk21N  39739  cdlemk20  39740  cdlemk22  39759  cdlemk26-3  39772  cdlemk27-3  39773  cdlemk28-3  39774  cdlemkfid3N  39791  cdlemk11ta  39795  cdlemk47  39815  cdlemk54  39824  dia2dimlem1  39930  dochsat  40249  dochshpncl  40250  lclkrlem2b  40374  lcfrlem21  40429  baerlem5amN  40582  baerlem5bmN  40583  baerlem5abmN  40584  mapdindp4  40589  mapdheq2  40595  mapdheq2biN  40596  mapdh6aN  40601  mapdh6dN  40605  mapdh6eN  40606  mapdh6hN  40609  mapdh7eN  40614  mapdh7dN  40616  mapdh7fN  40617  mapdh8ab  40643  mapdh8ad  40645  mapdh8e  40650  mapdh9a  40655  mapdh9aOLDN  40656  hdmap1l6a  40675  hdmap1l6d  40679  hdmap1l6e  40680  hdmap1l6h  40683  hdmap1eulem  40688  hdmap1eulemOLDN  40689  hdmapval0  40699  hdmapeveclem  40700  hdmapval3lemN  40703  hdmap10lem  40705  hdmap11lem1  40707  hdmaprnlem3N  40716  hdmaprnlem9N  40723  hdmaprnlem3eN  40724  fzne2d  40841  lcmineqlem11  40899  3lexlogpow5ineq1  40914  3lexlogpow5ineq2  40915  3lexlogpow5ineq4  40916  3lexlogpow5ineq3  40917  3lexlogpow2ineq1  40918  3lexlogpow2ineq2  40919  3lexlogpow5ineq5  40920  aks4d1lem1  40922  dvrelog2b  40926  dvrelogpow2b  40928  aks4d1p1p3  40929  aks4d1p1p2  40930  aks4d1p1p4  40931  aks4d1p1p6  40933  aks4d1p1p7  40934  aks4d1p1p5  40935  aks4d1p1  40936  aks4d1p2  40937  aks4d1p3  40938  aks4d1p5  40940  aks4d1p6  40941  aks4d1p7d1  40942  aks4d1p7  40943  aks4d1p8d3  40946  aks4d1p8  40947  aks4d1p9  40948  fldhmf1  40950  aks6d1c2p2  40952  2np3bcnp1  40955  2ap1caineq  40956  sticksstones1  40957  sticksstones2  40958  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  sticksstones22  40979  metakunt7  40986  metakunt12  40991  metakunt22  41001  xppss12  41049  mhpind  41168  jm2.26lem3  41730  rpnnen3lem  41760  rpnnen3  41761  imo72b2lem0  42907  imo72b2lem2  42909  imo72b2  42914  mnuprdlem1  43021  bcc0  43089  chordthmALT  43684  fnchoice  43703  refsum2cnlem1  43711  xrleneltd  44023  xrltned  44057  infleinf  44072  reclt0  44091  icoiccdif  44227  ressiooinf  44260  limcresiooub  44348  limcleqr  44350  limclner  44357  climxrre  44456  icccncfext  44593  cncfiooiccre  44601  dvnxpaek  44648  stoweidlem43  44749  stirlinglem5  44784  stirlinglem7  44786  dirkercncflem1  44809  fourierdlem24  44837  fourierdlem32  44845  fourierdlem33  44846  fourierdlem34  44847  fourierdlem35  44848  fourierdlem46  44858  fourierdlem48  44860  fourierdlem49  44861  fourierdlem64  44876  fourierdlem65  44877  fourierdlem74  44886  fourierdlem76  44888  fourierdlem79  44891  fourierdlem81  44893  fourierdlem91  44903  fourierdlem102  44914  fourierdlem114  44926  etransclem15  44955  etransclem24  44964  sge0rpcpnf  45127  sge0isum  45133  pimrecltpos  45414  pimiooltgt  45416  setsnidel  46035  odz2prm2pw  46221  fmtnoprmfac1lem  46222  fmtnoprmfac1  46223  fmtnoprmfac2  46225  lighneallem1  46263  lighneallem3  46265  perfectALTVlem2  46380  nnsgrpnmnd  46578  nrhmzr  46637  lvecpsslmod  47178  affinecomb1  47378  affinecomb2  47379  1subrec1sub  47381  rrx2plord2  47398  line  47408  rrxline  47410  eenglngeehlnmlem2  47414  rrx2vlinest  47417  line2xlem  47429  2itscp  47457