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

Theorem necomd 2650
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 2648 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 189 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2567
This theorem is referenced by:  difsnb  3900  0nelop  4406  difsnen  7149  fofinf1o  7346  ackbij1lem15  8070  infpssrlem5  8143  fin23lem24  8158  fin23lem31  8179  isf32lem9  8197  canthnumlem  8479  canthp1lem2  8484  npomex  8829  ltned  9165  lt0ne0  9450  recgt0  9810  zneo  10308  xrltne  10709  supxrbnd  10863  seqf1olem1  11317  nn0opthi  11518  hashtpg  11646  cats1un  11745  geoserg  12600  geolim  12602  geolim2  12603  tanadd  12723  ruclem6  12789  ruclem7  12790  isprm5  13067  oddprm  13144  pcmpt  13216  mrissmrcd  13820  dprdcntz  15521  dprdres  15541  ablfac1b  15583  lbspss  16109  lspsnnecom  16146  lspindp2l  16161  lspindp2  16162  islbs3  16182  lbsextlem4  16188  sralem  16204  lidlnz  16254  psrridm  16423  coe1tmfv2  16622  coe1tmmul  16624  en2top  17005  cmpfi  17425  snfil  17849  tsmsfbas  18110  zcld  18797  iccpnfhmeo  18923  xrhmeo  18924  evth  18937  minveclem3b  19282  i1fres  19550  dvcnvlem  19813  ig1peu  20047  ig1pdvds  20052  aaliou3lem9  20220  taylthlem2  20243  abelthlem2  20301  abelthlem7  20307  tanregt0  20394  logne0  20450  logcj  20454  argimgt0  20460  dvloglem  20492  logf1o2  20494  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  ang180lem5  20608  ang180  20609  isosctrlem3  20617  ssscongptld  20619  angpieqvdlem  20622  angpieqvdlem2  20623  angpieqvd  20625  chordthmlem  20626  chordthmlem2  20627  chordthm  20631  asinneg  20679  ppiltx  20913  perfectlem2  20967  lgsneg  21056  lgsqr  21083  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem3  21093  lgsquad2  21097  dchrisum0flblem1  21155  umgraex  21311  isusgra0  21329  usgra1v  21362  cyclnspth  21571  4cycl4dv  21607  vdgr1a  21630  eupap1  21651  eupath2lem3  21654  staddi  23702  ofldlt1  24196  ofldchr  24197  logbrec  24358  cntnevol  24535  derangenlem  24810  subfacp1lem1  24818  subfacp1lem3  24821  subfacp1lem5  24823  nodenselem3  25551  dfrdg4  25703  brbtwn2  25748  axlowdimlem15  25799  axlowdimlem16  25800  axcontlem8  25814  ifscgr  25882  cgrxfr  25893  btwnconn1lem8  25932  btwnconn3  25941  segcon2  25943  broutsideof3  25964  outsideoftr  25967  outsideofeq  25968  outsideofeu  25969  lineunray  25985  lineelsb2  25986  linethru  25991  itg2addnclem2  26156  ftc1cnnc  26178  heibor1lem  26408  maxidln0  26545  jm2.26lem3  26962  rpnnen3lem  26992  rpnnen3  26993  uvcf1  27109  frlmup2  27119  en2eleq  27249  en2other2  27250  pmtrprfv  27264  symggen  27279  mamulid  27326  fnchoice  27567  refsum2cnlem1  27575  stoweidlem43  27659  stirlinglem5  27694  stirlinglem7  27696  2spot2iun2spont  28088  1to3vfriswmgra  28111  frghash2spot  28166  chordthmALT  28755  lshpnelb  29467  lsatssn0  29485  lsatcv0  29514  lsat0cv  29516  lsatexch1  29529  l1cvat  29538  atlen0  29793  cvlsupr2  29826  atcvrj2b  29914  2atlt  29921  atbtwn  29928  3noncolr2  29931  4noncolr3  29935  3dimlem3  29943  3dimlem3OLDN  29944  3dimlem4  29946  3dimlem4OLDN  29947  3dim2  29950  1cvratex  29955  1cvrat  29958  ps-1  29959  ps-2  29960  hlatexch4  29963  3atlem4  29968  3atlem6  29970  4atlem0ae  30076  4atlem0be  30077  dalemccnedd  30169  dalemrotps  30173  dalem21  30176  dalem23  30178  dalem27  30181  dalem41  30195  dalem44  30198  dalem54  30208  lnatexN  30261  lnjatN  30262  llnexchb2lem  30350  llnexchb2  30351  lhpn0  30486  lhpexle3lem  30493  lhpmatb  30513  4atexlemswapqr  30545  4atexlemc  30551  4atexlemnclw  30552  4atexlemcnd  30554  4atexlemex4  30555  4atexlemex6  30556  4atex  30558  trlat  30651  trlval4  30670  cdlemc5  30677  cdlemd4  30683  cdlemd7  30686  cdlemd9  30688  cdleme0e  30699  cdleme3b  30711  cdleme3c  30712  cdleme3e  30714  cdleme3h  30717  cdleme7aa  30724  cdleme7e  30729  cdleme7ga  30730  cdleme9  30735  cdleme11c  30743  cdleme11e  30745  cdleme11fN  30746  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme15b  30757  cdleme15c  30758  cdleme17c  30770  cdleme18b  30774  cdlemesner  30778  cdleme20zN  30783  cdleme19c  30787  cdleme19d  30788  cdleme19e  30789  cdleme20m  30805  cdleme21a  30807  cdleme21b  30808  cdleme21c  30809  cdleme22f2  30829  cdleme28b  30853  cdleme36a  30942  cdleme36m  30943  cdleme41sn4aw  30957  cdleme43bN  30972  cdleme43dN  30974  cdleme46f2g2  30975  cdleme46f2g1  30976  cdleme4gfv  30989  cdlemeg46nlpq  30999  cdlemeg46req  31011  cdlemeg46fgN  31016  cdlemf1  31043  cdlemg8b  31110  cdlemg9a  31114  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg17pq  31154  cdlemg18a  31160  cdlemg18c  31162  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg31b0N  31176  cdlemg31b0a  31177  cdlemg31c  31181  cdlemg33b0  31183  cdlemg33c0  31184  trlcone  31210  cdlemg42  31211  cdlemg44a  31213  cdlemg46  31217  cdlemh1  31297  cdlemh2  31298  cdlemh  31299  cdlemj3  31305  cdlemk3  31315  cdlemki  31323  cdlemksv2  31329  cdlemk12  31332  cdlemk14  31336  cdlemk15  31337  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk21N  31355  cdlemk20  31356  cdlemk22  31375  cdlemk26-3  31388  cdlemk27-3  31389  cdlemk28-3  31390  cdlemkfid3N  31407  cdlemk11ta  31411  cdlemk47  31431  cdlemk54  31440  dia2dimlem1  31547  dochsat  31866  dochshpncl  31867  lclkrlem2b  31991  lcfrlem21  32046  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdindp4  32206  mapdheq2  32212  mapdheq2biN  32213  mapdh6aN  32218  mapdh6dN  32222  mapdh6eN  32223  mapdh6hN  32226  mapdh7eN  32231  mapdh7dN  32233  mapdh7fN  32234  mapdh8ab  32260  mapdh8ad  32262  mapdh8e  32267  mapdh9a  32273  mapdh9aOLDN  32274  hdmap1l6a  32293  hdmap1l6d  32297  hdmap1l6e  32298  hdmap1l6h  32301  hdmap1eulem  32307  hdmap1eulemOLDN  32308  hdmapval0  32319  hdmapeveclem  32320  hdmapval3lemN  32323  hdmap10lem  32325  hdmap11lem1  32327  hdmaprnlem3N  32336  hdmaprnlem9N  32343  hdmaprnlem3eN  32344
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397  df-ne 2569
  Copyright terms: Public domain W3C validator