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

Theorem necomd 2542
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 2540 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 188 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2459
This theorem is referenced by:  difsnb  3773  0nelop  4272  difsnen  6960  fofinf1o  7153  ackbij1lem15  7876  infpssrlem5  7949  fin23lem24  7964  fin23lem31  7985  isf32lem9  8003  canth4  8285  canthnumlem  8286  canthp1lem2  8291  npomex  8636  ltned  8971  lt0ne0  9256  recgt0  9616  zneo  10110  xrltne  10510  supxrbnd  10663  seqf1olem1  11101  nn0opthi  11301  cats1un  11492  geoserg  12340  geolim  12342  geolim2  12343  tanadd  12463  ruclem6  12529  ruclem7  12530  isprm5  12807  oddprm  12884  pcmpt  12956  mrissmrcd  13558  dprdcntz  15259  dprdres  15279  ablfac1b  15321  lbspss  15851  lspsnnecom  15888  lspindp2l  15903  lspindp2  15904  islbs3  15924  lbsextlem4  15930  sralem  15946  lidlnz  15996  psrridm  16165  coe1tmfv2  16367  coe1tmmul  16369  en2top  16739  cmpfi  17151  snfil  17575  tsmsfbas  17826  zcld  18335  iccpnfhmeo  18459  xrhmeo  18460  evth  18473  minveclem3b  18808  i1fres  19076  dvcnvlem  19339  ig1peu  19573  ig1pdvds  19578  aaliou3lem9  19746  taylthlem2  19769  abelthlem2  19824  abelthlem7  19830  tanregt0  19917  logne0  19972  logcj  19976  argimgt0  19982  dvloglem  20011  logf1o2  20013  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  ang180lem5  20127  ang180  20128  isosctrlem3  20136  ssscongptld  20138  angpieqvdlem  20141  angpieqvdlem2  20142  angpieqvd  20144  chordthmlem  20145  chordthmlem2  20146  chordthm  20150  asinneg  20198  ppiltx  20431  perfectlem2  20485  lgsneg  20574  lgsqr  20601  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem3  20611  lgsquad2  20615  dchrisum0flblem1  20673  staddi  22842  bcm1n  23048  cntnevol  23191  xrge0iifhom  23334  logbrec  23422  derangenlem  23717  subfacp1lem1  23725  subfacp1lem3  23728  subfacp1lem5  23730  umgraex  23890  vdgr1a  23912  eupap1  23915  eupath2lem3  23918  nodenselem3  24408  dfrdg4  24560  brbtwn2  24605  axlowdimlem13  24654  axlowdimlem15  24656  axlowdimlem16  24657  axcontlem8  24671  ifscgr  24739  cgrxfr  24750  btwnconn1lem8  24789  btwnconn3  24798  segcon2  24800  broutsideof3  24821  outsideoftr  24824  outsideofeq  24825  outsideofeu  24826  lineunray  24842  lineelsb2  24843  linethru  24848  itg2addnclem2  25004  ftc1cnnc  25025  usinuniopb  25697  dmse2  25707  xsyysx  26248  heibor1lem  26636  maxidln0  26773  jm2.26lem3  27197  rpnnen3lem  27227  rpnnen3  27228  uvcf1  27344  frlmup2  27354  en2eleq  27484  en2other2  27485  pmtrprfv  27499  symggen  27514  mamulid  27561  fnchoice  27803  refsum2cnlem1  27811  stoweidlem43  27895  wallispilem4  27920  wallispi  27922  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem14  27939  stirlinglem15  27940  hashtpg  28217  isusgra0  28238  usgra1v  28260  cyclnspth  28376  4cycl4dv  28413  1to3vfriswmgra  28431  chordthmALT  29026  lshpnelb  29796  lsatssn0  29814  lsatcv0  29843  lsat0cv  29845  lsatexch1  29858  l1cvat  29867  atlen0  30122  cvlsupr2  30155  atcvrj2b  30243  2atlt  30250  atbtwn  30257  3noncolr2  30260  4noncolr3  30264  3dimlem3  30272  3dimlem3OLDN  30273  3dimlem4  30275  3dimlem4OLDN  30276  3dim2  30279  1cvratex  30284  1cvrat  30287  ps-1  30288  ps-2  30289  hlatexch4  30292  3atlem4  30297  3atlem6  30299  4atlem0ae  30405  4atlem0be  30406  dalemccnedd  30498  dalemrotps  30502  dalem21  30505  dalem23  30507  dalem27  30510  dalem41  30524  dalem44  30527  dalem54  30537  lnatexN  30590  lnjatN  30591  llnexchb2lem  30679  llnexchb2  30680  lhpn0  30815  lhpexle3lem  30822  lhpmatb  30842  4atexlemswapqr  30874  4atexlemc  30880  4atexlemnclw  30881  4atexlemcnd  30883  4atexlemex4  30884  4atexlemex6  30885  4atex  30887  trlat  30980  trlval4  30999  cdlemc5  31006  cdlemd4  31012  cdlemd7  31015  cdlemd9  31017  cdleme0e  31028  cdleme3b  31040  cdleme3c  31041  cdleme3e  31043  cdleme3h  31046  cdleme7aa  31053  cdleme7e  31058  cdleme7ga  31059  cdleme9  31064  cdleme11c  31072  cdleme11e  31074  cdleme11fN  31075  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme15b  31086  cdleme15c  31087  cdleme17c  31099  cdleme18b  31103  cdlemesner  31107  cdleme20zN  31112  cdleme19c  31116  cdleme19d  31117  cdleme19e  31118  cdleme20m  31134  cdleme21a  31136  cdleme21b  31137  cdleme21c  31138  cdleme22f2  31158  cdleme28b  31182  cdleme36a  31271  cdleme36m  31272  cdleme41sn4aw  31286  cdleme43bN  31301  cdleme43dN  31303  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme4gfv  31318  cdlemeg46nlpq  31328  cdlemeg46req  31340  cdlemeg46fgN  31345  cdlemf1  31372  cdlemg8b  31439  cdlemg9a  31443  cdlemg12g  31460  cdlemg12  31461  cdlemg13a  31462  cdlemg17pq  31483  cdlemg18a  31489  cdlemg18c  31491  cdlemg19a  31494  cdlemg19  31495  cdlemg21  31497  cdlemg31b0N  31505  cdlemg31b0a  31506  cdlemg31c  31510  cdlemg33b0  31512  cdlemg33c0  31513  trlcone  31539  cdlemg42  31540  cdlemg44a  31542  cdlemg46  31546  cdlemh1  31626  cdlemh2  31627  cdlemh  31628  cdlemj3  31634  cdlemk3  31644  cdlemki  31652  cdlemksv2  31658  cdlemk12  31661  cdlemk14  31665  cdlemk15  31666  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  cdlemk22  31704  cdlemk26-3  31717  cdlemk27-3  31718  cdlemk28-3  31719  cdlemkfid3N  31736  cdlemk11ta  31740  cdlemk47  31760  cdlemk54  31769  dia2dimlem1  31876  dochsat  32195  dochshpncl  32196  lclkrlem2b  32320  lcfrlem21  32375  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdindp4  32535  mapdheq2  32541  mapdheq2biN  32542  mapdh6aN  32547  mapdh6dN  32551  mapdh6eN  32552  mapdh6hN  32555  mapdh7eN  32560  mapdh7dN  32562  mapdh7fN  32563  mapdh8ab  32589  mapdh8ad  32591  mapdh8e  32596  mapdh9a  32602  mapdh9aOLDN  32603  hdmap1l6a  32622  hdmap1l6d  32626  hdmap1l6e  32627  hdmap1l6h  32630  hdmap1eulem  32636  hdmap1eulemOLDN  32637  hdmapval0  32648  hdmapeveclem  32649  hdmapval3lemN  32652  hdmap10lem  32654  hdmap11lem1  32656  hdmaprnlem3N  32665  hdmaprnlem9N  32672  hdmaprnlem3eN  32673
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator