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

Theorem necomd 2694
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 2692 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 196 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2607
This theorem is referenced by:  difsnb  4014  0nelop  4580  xpdifid  5265  difsnen  7392  fofinf1o  7591  en2eleq  8174  en2other2  8175  ackbij1lem15  8402  infpssrlem5  8475  fin23lem24  8490  fin23lem31  8511  isf32lem9  8529  canthnumlem  8814  canthp1lem2  8819  npomex  9164  ltned  9509  lt0ne0  9804  recgt0  10172  zneo  10723  xrltne  11136  supxrbnd  11290  seqf1olem1  11844  nn0opthi  12047  hashtpg  12185  hashge3el3dif  12186  cats1un  12369  geoserg  13327  geolim  13329  geolim2  13330  tanadd  13450  ruclem6  13516  ruclem7  13517  isprm5  13797  oddprm  13881  pcmpt  13953  cshwshashlem3  14123  mrissmrcd  14577  pmtrprfv  15958  symggen  15975  dprdcntz  16491  dprdres  16524  ablfac1b  16570  lbspss  17162  lspsnnecom  17199  lspindp2l  17214  lspindp2  17215  islbs3  17235  lbsextlem4  17241  sralem  17257  lidlnz  17309  psrridm  17475  psrridmOLD  17476  coe1tmfv2  17727  coe1tmmul  17729  uvcf1  18216  frlmup2  18226  mdetralt  18413  mdetunilem2  18418  mdetunilem6  18422  mdetunilem7  18423  maducoeval2  18445  madurid  18449  en2top  18589  cmpfi  19010  snfil  19436  tsmsfbas  19697  zcld  20389  iccpnfhmeo  20516  xrhmeo  20517  evth  20530  minveclem3b  20914  i1fres  21182  dvcnvlem  21447  ig1peu  21642  ig1pdvds  21647  aaliou3lem9  21815  taylthlem2  21838  abelthlem2  21896  abelthlem7  21902  tanregt0  21994  logne0  22050  logcj  22054  argimgt0  22060  dvloglem  22092  logf1o2  22094  ang180lem1  22204  ang180lem2  22205  ang180lem3  22206  ang180lem4  22207  ang180lem5  22208  ang180  22209  isosctrlem3  22217  ssscongptld  22219  angpieqvdlem  22222  angpieqvdlem2  22223  angpieqvd  22225  chordthmlem  22226  chordthmlem2  22227  chordthm  22231  asinneg  22280  ppiltx  22514  perfectlem2  22568  lgsneg  22657  lgsqr  22684  lgseisenlem4  22690  lgsquadlem1  22692  lgsquadlem3  22694  lgsquad2  22698  dchrisum0flblem1  22756  tgbtwnouttr  22949  tgifscgr  22960  tgcgrxfr  22969  tglngval  22984  tgfscgr  22999  tgbtwnconn1lem3  23005  tgbtwnconn3  23008  legtrid  23021  lncom  23028  tgisline  23033  tglineeltr  23036  tglineelsb2  23037  tglinecom  23040  tglinethru  23041  ncolncol  23050  symquadlem  23082  midexlem  23085  ragcol  23092  ragcgr  23100  perpneq  23104  footex  23108  foot  23109  ttgcontlem1  23130  cchhllem  23132  brbtwn2  23150  axlowdimlem15  23201  axlowdimlem16  23202  axcontlem8  23216  umgraex  23256  isusgra0  23274  usgra1v  23307  cyclnspth  23516  4cycl4dv  23552  vdgr1a  23575  eupap1  23596  eupath2lem3  23599  staddi  25649  ornglmullt  26274  orngrmullt  26275  orngmullt  26276  ofldlt1  26280  ofldchr  26281  isarchiofld  26284  ordtconlem1  26353  logbrec  26463  cntnevol  26641  sgnmul  26924  sgn0bi  26929  sgnmulsgp  26932  signstfveq0a  26976  signsvfpn  26985  derangenlem  27058  subfacp1lem1  27066  subfacp1lem3  27069  subfacp1lem5  27071  nodenselem3  27823  dfrdg4  27980  ifscgr  28074  cgrxfr  28085  btwnconn1lem8  28124  btwnconn3  28133  segcon2  28135  broutsideof3  28156  outsideoftr  28159  outsideofeq  28160  outsideofeu  28161  lineunray  28177  lineelsb2  28178  linethru  28183  fin2solem  28413  dvtanlem  28439  itg2addnclem2  28442  ftc1cnnc  28464  heibor1lem  28706  maxidln0  28843  jm2.26lem3  29348  rpnnen3lem  29378  rpnnen3  29379  fnchoice  29749  refsum2cnlem1  29757  stoweidlem43  29836  stirlinglem5  29871  stirlinglem7  29873  2spot2iun2spont  30408  usg2cwwk2dif  30492  1to3vfriswmgra  30597  frghash2spot  30654  01eq0rng  30775  dmatmul  30874  lvecpsslmod  31047  chordthmALT  31667  bj-bary1lem  32597  bj-bary1lem1  32598  bj-bary1  32599  lshpnelb  32627  lsatssn0  32645  lsatcv0  32674  lsat0cv  32676  lsatexch1  32689  l1cvat  32698  atlen0  32953  cvlsupr2  32986  atcvrj2b  33074  2atlt  33081  atbtwn  33088  3noncolr2  33091  4noncolr3  33095  3dimlem3  33103  3dimlem3OLDN  33104  3dimlem4  33106  3dimlem4OLDN  33107  3dim2  33110  1cvratex  33115  1cvrat  33118  ps-1  33119  ps-2  33120  hlatexch4  33123  3atlem4  33128  3atlem6  33130  4atlem0ae  33236  4atlem0be  33237  dalemccnedd  33329  dalemrotps  33333  dalem21  33336  dalem23  33338  dalem27  33341  dalem41  33355  dalem44  33358  dalem54  33368  lnatexN  33421  lnjatN  33422  llnexchb2lem  33510  llnexchb2  33511  lhpn0  33646  lhpexle3lem  33653  lhpmatb  33673  4atexlemswapqr  33705  4atexlemc  33711  4atexlemnclw  33712  4atexlemcnd  33714  4atexlemex4  33715  4atexlemex6  33716  4atex  33718  trlat  33811  trlval4  33830  cdlemc5  33837  cdlemd4  33843  cdlemd7  33846  cdlemd9  33848  cdleme0e  33859  cdleme3b  33871  cdleme3c  33872  cdleme3e  33874  cdleme3h  33877  cdleme7aa  33884  cdleme7e  33889  cdleme7ga  33890  cdleme9  33895  cdleme11c  33903  cdleme11e  33905  cdleme11fN  33906  cdleme11h  33908  cdleme11j  33909  cdleme11k  33910  cdleme15b  33917  cdleme15c  33918  cdleme17c  33930  cdleme18b  33934  cdlemesner  33938  cdleme20zN  33943  cdleme19c  33947  cdleme19d  33948  cdleme19e  33949  cdleme20m  33965  cdleme21a  33967  cdleme21b  33968  cdleme21c  33969  cdleme22f2  33989  cdleme28b  34013  cdleme36a  34102  cdleme36m  34103  cdleme41sn4aw  34117  cdleme43bN  34132  cdleme43dN  34134  cdleme46f2g2  34135  cdleme46f2g1  34136  cdleme4gfv  34149  cdlemeg46nlpq  34159  cdlemeg46req  34171  cdlemeg46fgN  34176  cdlemf1  34203  cdlemg8b  34270  cdlemg9a  34274  cdlemg12g  34291  cdlemg12  34292  cdlemg13a  34293  cdlemg17pq  34314  cdlemg18a  34320  cdlemg18c  34322  cdlemg19a  34325  cdlemg19  34326  cdlemg21  34328  cdlemg31b0N  34336  cdlemg31b0a  34337  cdlemg31c  34341  cdlemg33b0  34343  cdlemg33c0  34344  trlcone  34370  cdlemg42  34371  cdlemg44a  34373  cdlemg46  34377  cdlemh1  34457  cdlemh2  34458  cdlemh  34459  cdlemj3  34465  cdlemk3  34475  cdlemki  34483  cdlemksv2  34489  cdlemk12  34492  cdlemk14  34496  cdlemk15  34497  cdlemk7u  34512  cdlemk11u  34513  cdlemk12u  34514  cdlemk21N  34515  cdlemk20  34516  cdlemk22  34535  cdlemk26-3  34548  cdlemk27-3  34549  cdlemk28-3  34550  cdlemkfid3N  34567  cdlemk11ta  34571  cdlemk47  34591  cdlemk54  34600  dia2dimlem1  34707  dochsat  35026  dochshpncl  35027  lclkrlem2b  35151  lcfrlem21  35206  baerlem5amN  35359  baerlem5bmN  35360  baerlem5abmN  35361  mapdindp4  35366  mapdheq2  35372  mapdheq2biN  35373  mapdh6aN  35378  mapdh6dN  35382  mapdh6eN  35383  mapdh6hN  35386  mapdh7eN  35391  mapdh7dN  35393  mapdh7fN  35394  mapdh8ab  35420  mapdh8ad  35422  mapdh8e  35427  mapdh9a  35433  mapdh9aOLDN  35434  hdmap1l6a  35453  hdmap1l6d  35457  hdmap1l6e  35458  hdmap1l6h  35461  hdmap1eulem  35467  hdmap1eulemOLDN  35468  hdmapval0  35479  hdmapeveclem  35480  hdmapval3lemN  35483  hdmap10lem  35485  hdmap11lem1  35487  hdmaprnlem3N  35496  hdmaprnlem9N  35503  hdmaprnlem3eN  35504
  Copyright terms: Public domain W3C validator