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

Theorem necomd 2529
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 2527 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 188 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2446
This theorem is referenced by:  difsneq  3757  0nelop  4256  difsnen  6944  fofinf1o  7137  ackbij1lem15  7860  infpssrlem5  7933  fin23lem24  7948  fin23lem31  7969  isf32lem9  7987  canth4  8269  canthnumlem  8270  canthp1lem2  8275  npomex  8620  ltned  8955  lt0ne0  9240  recgt0  9600  zneo  10094  xrltne  10494  supxrbnd  10647  seqf1olem1  11085  nn0opthi  11285  cats1un  11476  geoserg  12324  geolim  12326  geolim2  12327  tanadd  12447  ruclem6  12513  ruclem7  12514  isprm5  12791  oddprm  12868  pcmpt  12940  mrissmrcd  13542  dprdcntz  15243  dprdres  15263  ablfac1b  15305  lbspss  15835  lspsnnecom  15872  lspindp2l  15887  lspindp2  15888  islbs3  15908  lbsextlem4  15914  sralem  15930  lidlnz  15980  psrridm  16149  coe1tmfv2  16351  coe1tmmul  16353  en2top  16723  cmpfi  17135  snfil  17559  tsmsfbas  17810  zcld  18319  iccpnfhmeo  18443  xrhmeo  18444  evth  18457  minveclem3b  18792  i1fres  19060  dvcnvlem  19323  ig1peu  19557  ig1pdvds  19562  aaliou3lem9  19730  taylthlem2  19753  abelthlem2  19808  abelthlem7  19814  tanregt0  19901  logne0  19956  logcj  19960  argimgt0  19966  dvloglem  19995  logf1o2  19997  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  ang180lem4  20110  ang180lem5  20111  ang180  20112  isosctrlem3  20120  ssscongptld  20122  angpieqvdlem  20125  angpieqvdlem2  20126  angpieqvd  20128  chordthmlem  20129  chordthmlem2  20130  chordthm  20134  asinneg  20182  ppiltx  20415  perfectlem2  20469  lgsneg  20558  lgsqr  20585  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem3  20595  lgsquad2  20599  dchrisum0flblem1  20657  staddi  22826  bcm1n  23032  cntnevol  23175  xrge0iifhom  23319  logbrec  23407  derangenlem  23702  subfacp1lem1  23710  subfacp1lem3  23713  subfacp1lem5  23715  umgraex  23875  vdgr1a  23897  eupap1  23900  eupath2lem3  23903  nodenselem3  24337  dfrdg4  24488  brbtwn2  24533  axlowdimlem13  24582  axlowdimlem15  24584  axlowdimlem16  24585  axcontlem8  24599  ifscgr  24667  cgrxfr  24678  btwnconn1lem8  24717  btwnconn3  24726  segcon2  24728  broutsideof3  24749  outsideoftr  24752  outsideofeq  24753  outsideofeu  24754  lineunray  24770  lineelsb2  24771  linethru  24776  usinuniopb  25594  dmse2  25604  xsyysx  26145  heibor1lem  26533  maxidln0  26670  jm2.26lem3  27094  rpnnen3lem  27124  rpnnen3  27125  uvcf1  27241  frlmup2  27251  en2eleq  27381  en2other2  27382  pmtrprfv  27396  symggen  27411  mamulid  27458  fnchoice  27700  refsum2cnlem1  27708  stoweidlem43  27792  wallispilem4  27817  wallispi  27819  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem14  27836  stirlinglem15  27837  isusgra0  28106  usgra1v  28126  1to3vfriswmgra  28185  chordthmALT  28710  lshpnelb  29174  lsatssn0  29192  lsatcv0  29221  lsat0cv  29223  lsatexch1  29236  l1cvat  29245  atlen0  29500  cvlsupr2  29533  atcvrj2b  29621  2atlt  29628  atbtwn  29635  3noncolr2  29638  4noncolr3  29642  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4  29653  3dimlem4OLDN  29654  3dim2  29657  1cvratex  29662  1cvrat  29665  ps-1  29666  ps-2  29667  hlatexch4  29670  3atlem4  29675  3atlem6  29677  4atlem0ae  29783  4atlem0be  29784  dalemccnedd  29876  dalemrotps  29880  dalem21  29883  dalem23  29885  dalem27  29888  dalem41  29902  dalem44  29905  dalem54  29915  lnatexN  29968  lnjatN  29969  llnexchb2lem  30057  llnexchb2  30058  lhpn0  30193  lhpexle3lem  30200  lhpmatb  30220  4atexlemswapqr  30252  4atexlemc  30258  4atexlemnclw  30259  4atexlemcnd  30261  4atexlemex4  30262  4atexlemex6  30263  4atex  30265  trlat  30358  trlval4  30377  cdlemc5  30384  cdlemd4  30390  cdlemd7  30393  cdlemd9  30395  cdleme0e  30406  cdleme3b  30418  cdleme3c  30419  cdleme3e  30421  cdleme3h  30424  cdleme7aa  30431  cdleme7e  30436  cdleme7ga  30437  cdleme9  30442  cdleme11c  30450  cdleme11e  30452  cdleme11fN  30453  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme15b  30464  cdleme15c  30465  cdleme17c  30477  cdleme18b  30481  cdlemesner  30485  cdleme20zN  30490  cdleme19c  30494  cdleme19d  30495  cdleme19e  30496  cdleme20m  30512  cdleme21a  30514  cdleme21b  30515  cdleme21c  30516  cdleme22f2  30536  cdleme28b  30560  cdleme36a  30649  cdleme36m  30650  cdleme41sn4aw  30664  cdleme43bN  30679  cdleme43dN  30681  cdleme46f2g2  30682  cdleme46f2g1  30683  cdleme4gfv  30696  cdlemeg46nlpq  30706  cdlemeg46req  30718  cdlemeg46fgN  30723  cdlemf1  30750  cdlemg8b  30817  cdlemg9a  30821  cdlemg12g  30838  cdlemg12  30839  cdlemg13a  30840  cdlemg17pq  30861  cdlemg18a  30867  cdlemg18c  30869  cdlemg19a  30872  cdlemg19  30873  cdlemg21  30875  cdlemg31b0N  30883  cdlemg31b0a  30884  cdlemg31c  30888  cdlemg33b0  30890  cdlemg33c0  30891  trlcone  30917  cdlemg42  30918  cdlemg44a  30920  cdlemg46  30924  cdlemh1  31004  cdlemh2  31005  cdlemh  31006  cdlemj3  31012  cdlemk3  31022  cdlemki  31030  cdlemksv2  31036  cdlemk12  31039  cdlemk14  31043  cdlemk15  31044  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemk22  31082  cdlemk26-3  31095  cdlemk27-3  31096  cdlemk28-3  31097  cdlemkfid3N  31114  cdlemk11ta  31118  cdlemk47  31138  cdlemk54  31147  dia2dimlem1  31254  dochsat  31573  dochshpncl  31574  lclkrlem2b  31698  lcfrlem21  31753  baerlem5amN  31906  baerlem5bmN  31907  baerlem5abmN  31908  mapdindp4  31913  mapdheq2  31919  mapdheq2biN  31920  mapdh6aN  31925  mapdh6dN  31929  mapdh6eN  31930  mapdh6hN  31933  mapdh7eN  31938  mapdh7dN  31940  mapdh7fN  31941  mapdh8ab  31967  mapdh8ad  31969  mapdh8e  31974  mapdh9a  31980  mapdh9aOLDN  31981  hdmap1l6a  32000  hdmap1l6d  32004  hdmap1l6e  32005  hdmap1l6h  32008  hdmap1eulem  32014  hdmap1eulemOLDN  32015  hdmapval0  32026  hdmapeveclem  32027  hdmapval3lemN  32030  hdmap10lem  32032  hdmap11lem1  32034  hdmaprnlem3N  32043  hdmaprnlem9N  32050  hdmaprnlem3eN  32051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator