MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necomd Structured version   Unicode version

Theorem necomd 2681
Description: Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
Hypothesis
Ref Expression
necomd.1  |-  ( ph  ->  A  =/=  B )
Assertion
Ref Expression
necomd  |-  ( ph  ->  B  =/=  A )

Proof of Theorem necomd
StepHypRef Expression
1 necomd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 necom 2679 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 189 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2598
This theorem is referenced by:  difsnb  3932  0nelop  4438  difsnen  7182  fofinf1o  7379  ackbij1lem15  8106  infpssrlem5  8179  fin23lem24  8194  fin23lem31  8215  isf32lem9  8233  canthnumlem  8515  canthp1lem2  8520  npomex  8865  ltned  9201  lt0ne0  9486  recgt0  9846  zneo  10344  xrltne  10745  supxrbnd  10899  seqf1olem1  11354  nn0opthi  11555  hashtpg  11683  cats1un  11782  geoserg  12637  geolim  12639  geolim2  12640  tanadd  12760  ruclem6  12826  ruclem7  12827  isprm5  13104  oddprm  13181  pcmpt  13253  mrissmrcd  13857  dprdcntz  15558  dprdres  15578  ablfac1b  15620  lbspss  16146  lspsnnecom  16183  lspindp2l  16198  lspindp2  16199  islbs3  16219  lbsextlem4  16225  sralem  16241  lidlnz  16291  psrridm  16460  coe1tmfv2  16659  coe1tmmul  16661  en2top  17042  cmpfi  17463  snfil  17888  tsmsfbas  18149  zcld  18836  iccpnfhmeo  18962  xrhmeo  18963  evth  18976  minveclem3b  19321  i1fres  19589  dvcnvlem  19852  ig1peu  20086  ig1pdvds  20091  aaliou3lem9  20259  taylthlem2  20282  abelthlem2  20340  abelthlem7  20346  tanregt0  20433  logne0  20489  logcj  20493  argimgt0  20499  dvloglem  20531  logf1o2  20533  ang180lem1  20643  ang180lem2  20644  ang180lem3  20645  ang180lem4  20646  ang180lem5  20647  ang180  20648  isosctrlem3  20656  ssscongptld  20658  angpieqvdlem  20661  angpieqvdlem2  20662  angpieqvd  20664  chordthmlem  20665  chordthmlem2  20666  chordthm  20670  asinneg  20718  ppiltx  20952  perfectlem2  21006  lgsneg  21095  lgsqr  21122  lgseisenlem4  21128  lgsquadlem1  21130  lgsquadlem3  21132  lgsquad2  21136  dchrisum0flblem1  21194  umgraex  21350  isusgra0  21368  usgra1v  21401  cyclnspth  21610  4cycl4dv  21646  vdgr1a  21669  eupap1  21690  eupath2lem3  21693  staddi  23741  ofldlt1  24235  ofldchr  24236  logbrec  24397  cntnevol  24574  derangenlem  24849  subfacp1lem1  24857  subfacp1lem3  24860  subfacp1lem5  24862  nodenselem3  25630  dfrdg4  25787  brbtwn2  25836  axlowdimlem15  25887  axlowdimlem16  25888  axcontlem8  25902  ifscgr  25970  cgrxfr  25981  btwnconn1lem8  26020  btwnconn3  26029  segcon2  26031  broutsideof3  26052  outsideoftr  26055  outsideofeq  26056  outsideofeu  26057  lineunray  26073  lineelsb2  26074  linethru  26079  itg2addnclem2  26247  ftc1cnnc  26269  heibor1lem  26509  maxidln0  26646  jm2.26lem3  27063  rpnnen3lem  27093  rpnnen3  27094  uvcf1  27209  frlmup2  27219  en2eleq  27349  en2other2  27350  pmtrprfv  27364  symggen  27379  mamulid  27426  fnchoice  27667  refsum2cnlem1  27675  stoweidlem43  27759  stirlinglem5  27794  stirlinglem7  27796  cshwssizelem4  28247  2spot2iun2spont  28311  1to3vfriswmgra  28334  frghash2spot  28389  chordthmALT  28982  lshpnelb  29719  lsatssn0  29737  lsatcv0  29766  lsat0cv  29768  lsatexch1  29781  l1cvat  29790  atlen0  30045  cvlsupr2  30078  atcvrj2b  30166  2atlt  30173  atbtwn  30180  3noncolr2  30183  4noncolr3  30187  3dimlem3  30195  3dimlem3OLDN  30196  3dimlem4  30198  3dimlem4OLDN  30199  3dim2  30202  1cvratex  30207  1cvrat  30210  ps-1  30211  ps-2  30212  hlatexch4  30215  3atlem4  30220  3atlem6  30222  4atlem0ae  30328  4atlem0be  30329  dalemccnedd  30421  dalemrotps  30425  dalem21  30428  dalem23  30430  dalem27  30433  dalem41  30447  dalem44  30450  dalem54  30460  lnatexN  30513  lnjatN  30514  llnexchb2lem  30602  llnexchb2  30603  lhpn0  30738  lhpexle3lem  30745  lhpmatb  30765  4atexlemswapqr  30797  4atexlemc  30803  4atexlemnclw  30804  4atexlemcnd  30806  4atexlemex4  30807  4atexlemex6  30808  4atex  30810  trlat  30903  trlval4  30922  cdlemc5  30929  cdlemd4  30935  cdlemd7  30938  cdlemd9  30940  cdleme0e  30951  cdleme3b  30963  cdleme3c  30964  cdleme3e  30966  cdleme3h  30969  cdleme7aa  30976  cdleme7e  30981  cdleme7ga  30982  cdleme9  30987  cdleme11c  30995  cdleme11e  30997  cdleme11fN  30998  cdleme11h  31000  cdleme11j  31001  cdleme11k  31002  cdleme15b  31009  cdleme15c  31010  cdleme17c  31022  cdleme18b  31026  cdlemesner  31030  cdleme20zN  31035  cdleme19c  31039  cdleme19d  31040  cdleme19e  31041  cdleme20m  31057  cdleme21a  31059  cdleme21b  31060  cdleme21c  31061  cdleme22f2  31081  cdleme28b  31105  cdleme36a  31194  cdleme36m  31195  cdleme41sn4aw  31209  cdleme43bN  31224  cdleme43dN  31226  cdleme46f2g2  31227  cdleme46f2g1  31228  cdleme4gfv  31241  cdlemeg46nlpq  31251  cdlemeg46req  31263  cdlemeg46fgN  31268  cdlemf1  31295  cdlemg8b  31362  cdlemg9a  31366  cdlemg12g  31383  cdlemg12  31384  cdlemg13a  31385  cdlemg17pq  31406  cdlemg18a  31412  cdlemg18c  31414  cdlemg19a  31417  cdlemg19  31418  cdlemg21  31420  cdlemg31b0N  31428  cdlemg31b0a  31429  cdlemg31c  31433  cdlemg33b0  31435  cdlemg33c0  31436  trlcone  31462  cdlemg42  31463  cdlemg44a  31465  cdlemg46  31469  cdlemh1  31549  cdlemh2  31550  cdlemh  31551  cdlemj3  31557  cdlemk3  31567  cdlemki  31575  cdlemksv2  31581  cdlemk12  31584  cdlemk14  31588  cdlemk15  31589  cdlemk7u  31604  cdlemk11u  31605  cdlemk12u  31606  cdlemk21N  31607  cdlemk20  31608  cdlemk22  31627  cdlemk26-3  31640  cdlemk27-3  31641  cdlemk28-3  31642  cdlemkfid3N  31659  cdlemk11ta  31663  cdlemk47  31683  cdlemk54  31692  dia2dimlem1  31799  dochsat  32118  dochshpncl  32119  lclkrlem2b  32243  lcfrlem21  32298  baerlem5amN  32451  baerlem5bmN  32452  baerlem5abmN  32453  mapdindp4  32458  mapdheq2  32464  mapdheq2biN  32465  mapdh6aN  32470  mapdh6dN  32474  mapdh6eN  32475  mapdh6hN  32478  mapdh7eN  32483  mapdh7dN  32485  mapdh7fN  32486  mapdh8ab  32512  mapdh8ad  32514  mapdh8e  32519  mapdh9a  32525  mapdh9aOLDN  32526  hdmap1l6a  32545  hdmap1l6d  32549  hdmap1l6e  32550  hdmap1l6h  32553  hdmap1eulem  32559  hdmap1eulemOLDN  32560  hdmapval0  32571  hdmapeveclem  32572  hdmapval3lemN  32575  hdmap10lem  32577  hdmap11lem1  32579  hdmaprnlem3N  32588  hdmaprnlem9N  32595  hdmaprnlem3eN  32596
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428  df-ne 2600
  Copyright terms: Public domain W3C validator