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

Theorem necomd 2714
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 2712 . 2  |-  ( A  =/=  B  <->  B  =/=  A )
31, 2sylib 196 1  |-  ( ph  ->  B  =/=  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640
This theorem is referenced by:  difsnb  4157  0nelop  4727  xpdifid  5425  difsnen  7601  fofinf1o  7803  en2eleq  8389  en2other2  8390  ackbij1lem15  8617  infpssrlem5  8690  fin23lem24  8705  fin23lem31  8726  isf32lem9  8744  canthnumlem  9029  canthp1lem2  9034  npomex  9377  ltned  9724  lt0ne0  10025  recgt0  10393  zneo  10952  xrltne  11377  supxrbnd  11531  seqf1olem1  12128  nn0opthi  12332  hashtpg  12505  hashge3el3dif  12506  cats1un  12683  geoserg  13659  geolim  13661  geolim2  13662  tanadd  13884  ruclem6  13950  ruclem7  13951  isprm5  14235  oddprm  14321  pcmpt  14393  cshwshashlem3  14564  mrissmrcd  15019  pmtrprfv  16457  symggen  16474  dprdcntz  17020  dprdres  17054  ablfac1b  17100  lbspss  17707  lspsnnecom  17744  lspindp2l  17759  lspindp2  17760  islbs3  17780  lbsextlem4  17786  sralem  17802  lidlnz  17855  01eq0ring  17899  psrridm  18037  psrridmOLD  18038  coe1tmfv2  18295  coe1tmmul  18297  uvcf1  18801  frlmup2  18811  dmatmul  18977  mdetralt  19088  mdetunilem2  19093  mdetunilem6  19097  mdetunilem7  19098  maducoeval2  19120  madurid  19124  fvmptnn04ifa  19329  en2top  19465  cmpfi  19886  snfil  20343  tsmsfbas  20604  zcld  21296  iccpnfhmeo  21423  xrhmeo  21424  evth  21437  minveclem3b  21821  i1fres  22090  dvcnvlem  22355  ig1peu  22550  ig1pdvds  22555  aaliou3lem9  22724  taylthlem2  22747  abelthlem2  22805  abelthlem7  22811  tanregt0  22904  logne0  22965  logcj  22969  argimgt0  22975  dvloglem  23007  logf1o2  23009  ang180lem1  23119  ang180lem2  23120  ang180lem3  23121  ang180lem4  23122  ang180lem5  23123  ang180  23124  isosctrlem3  23132  ssscongptld  23134  angpieqvdlem  23137  angpieqvdlem2  23138  angpieqvd  23140  chordthmlem  23141  chordthmlem2  23142  chordthm  23146  asinneg  23195  ppiltx  23429  perfectlem2  23483  lgsneg  23572  lgsqr  23599  lgseisenlem4  23605  lgsquadlem1  23607  lgsquadlem3  23609  lgsquad2  23613  dchrisum0flblem1  23671  tgbtwnouttr  23866  tgifscgr  23878  tgcgrxfr  23887  tglngval  23916  tgfscgr  23933  tgbtwnconn1lem3  23939  tgbtwnconn3  23942  legtrid  23956  hltr  23972  hlbtwn  23973  btwnhl1  23974  btwnhl  23976  lncom  23980  tgisline  23985  tglineeltr  23989  tglineelsb2  23990  tglinecom  23993  tglinethru  23994  ncolncol  24004  coltr  24005  coltr2  24006  coltr3  24007  symquadlem  24044  midexlem  24047  ragcol  24054  ragcgr  24062  perpneq  24069  footex  24073  foot  24074  footne  24075  colperpexlem3  24084  mideulem2  24086  opphllem  24087  midex  24089  opphllem1  24097  opphllem2  24098  opphllem3  24099  opphllem4  24100  opphllem5  24101  opphllem6  24102  lnopp2hpgb  24110  lmieu  24128  hypcgrlem1  24142  hypcgrlem2  24143  ttgcontlem1  24166  cchhllem  24168  brbtwn2  24186  axlowdimlem15  24237  axlowdimlem16  24238  axcontlem8  24252  umgraex  24301  isusgra0  24325  usgraop  24328  usgra1v  24368  cyclnspth  24609  4cycl4dv  24645  usg2cwwk2dif  24798  2spot2iun2spont  24869  vdgr1a  24884  eupap1  24954  eupath2lem3  24957  1to3vfriswmgra  24985  frghash2spot  25041  staddi  27143  ornglmullt  27775  orngrmullt  27776  orngmullt  27777  ofldlt1  27781  ofldchr  27782  isarchiofld  27785  ordtconlem1  27884  logbrec  27999  cntnevol  28177  signstfveq0a  28511  derangenlem  28593  subfacp1lem1  28601  subfacp1lem3  28604  subfacp1lem5  28606  nodenselem3  29419  dfrdg4  29576  ifscgr  29670  cgrxfr  29681  btwnconn1lem8  29720  btwnconn3  29729  segcon2  29731  broutsideof3  29752  outsideoftr  29755  outsideofeq  29756  outsideofeu  29757  lineunray  29773  lineelsb2  29774  linethru  29779  fin2solem  30015  dvtanlem  30040  itg2addnclem2  30043  ftc1cnnc  30065  heibor1lem  30281  maxidln0  30418  jm2.26lem3  30919  rpnnen3lem  30949  rpnnen3  30950  fnchoice  31358  refsum2cnlem1  31366  flltnz  31452  icoiccdif  31518  limcresiooub  31602  limcleqr  31604  limclner  31611  icccncfext  31644  cncfiooiccre  31652  dvnxpaek  31693  stoweidlem43  31779  stirlinglem5  31814  stirlinglem7  31816  dirkercncflem1  31839  fourierdlem24  31867  fourierdlem32  31875  fourierdlem33  31876  fourierdlem34  31877  fourierdlem35  31878  fourierdlem46  31889  fourierdlem48  31891  fourierdlem49  31892  fourierdlem64  31907  fourierdlem65  31908  fourierdlem74  31917  fourierdlem76  31919  fourierdlem79  31922  fourierdlem81  31924  fourierdlem91  31934  fourierdlem102  31945  fourierdlem114  31957  etransclem15  31986  etransclem24  31995  usgvad2edg  32365  nnsgrpnmnd  32459  estrres  32611  lvecpsslmod  32978  chordthmALT  33601  bj-bary1lem  34554  bj-bary1lem1  34555  bj-bary1  34556  lshpnelb  34584  lsatssn0  34602  lsatcv0  34631  lsat0cv  34633  lsatexch1  34646  l1cvat  34655  atlen0  34910  cvlsupr2  34943  atcvrj2b  35031  2atlt  35038  atbtwn  35045  3noncolr2  35048  4noncolr3  35052  3dimlem3  35060  3dimlem3OLDN  35061  3dimlem4  35063  3dimlem4OLDN  35064  3dim2  35067  1cvratex  35072  1cvrat  35075  ps-1  35076  ps-2  35077  hlatexch4  35080  3atlem4  35085  3atlem6  35087  4atlem0ae  35193  4atlem0be  35194  dalemccnedd  35286  dalemrotps  35290  dalem21  35293  dalem23  35295  dalem27  35298  dalem41  35312  dalem44  35315  dalem54  35325  lnatexN  35378  lnjatN  35379  llnexchb2lem  35467  llnexchb2  35468  lhpn0  35603  lhpexle3lem  35610  lhpmatb  35630  4atexlemswapqr  35662  4atexlemc  35668  4atexlemnclw  35669  4atexlemcnd  35671  4atexlemex4  35672  4atexlemex6  35673  4atex  35675  trlat  35769  trlval4  35788  cdlemc5  35795  cdlemd4  35801  cdlemd7  35804  cdlemd9  35806  cdleme0e  35817  cdleme3b  35829  cdleme3c  35830  cdleme3e  35832  cdleme3h  35835  cdleme7aa  35842  cdleme7e  35847  cdleme7ga  35848  cdleme9  35853  cdleme11c  35861  cdleme11e  35863  cdleme11fN  35864  cdleme11h  35866  cdleme11j  35867  cdleme11k  35868  cdleme15b  35875  cdleme15c  35876  cdleme17c  35888  cdleme18b  35892  cdlemesner  35896  cdleme20zN  35901  cdleme19c  35906  cdleme19d  35907  cdleme19e  35908  cdleme20m  35924  cdleme21a  35926  cdleme21b  35927  cdleme21c  35928  cdleme22f2  35948  cdleme28b  35972  cdleme36a  36061  cdleme36m  36062  cdleme41sn4aw  36076  cdleme43bN  36091  cdleme43dN  36093  cdleme46f2g2  36094  cdleme46f2g1  36095  cdleme4gfv  36108  cdlemeg46nlpq  36118  cdlemeg46req  36130  cdlemeg46fgN  36135  cdlemf1  36162  cdlemg8b  36229  cdlemg9a  36233  cdlemg12g  36250  cdlemg12  36251  cdlemg13a  36252  cdlemg17pq  36273  cdlemg18a  36279  cdlemg18c  36281  cdlemg19a  36284  cdlemg19  36285  cdlemg21  36287  cdlemg31b0N  36295  cdlemg31b0a  36296  cdlemg31c  36300  cdlemg33b0  36302  cdlemg33c0  36303  trlcone  36329  cdlemg42  36330  cdlemg44a  36332  cdlemg46  36336  cdlemh1  36416  cdlemh2  36417  cdlemh  36418  cdlemj3  36424  cdlemk3  36434  cdlemki  36442  cdlemksv2  36448  cdlemk12  36451  cdlemk14  36455  cdlemk15  36456  cdlemk7u  36471  cdlemk11u  36472  cdlemk12u  36473  cdlemk21N  36474  cdlemk20  36475  cdlemk22  36494  cdlemk26-3  36507  cdlemk27-3  36508  cdlemk28-3  36509  cdlemkfid3N  36526  cdlemk11ta  36530  cdlemk47  36550  cdlemk54  36559  dia2dimlem1  36666  dochsat  36985  dochshpncl  36986  lclkrlem2b  37110  lcfrlem21  37165  baerlem5amN  37318  baerlem5bmN  37319  baerlem5abmN  37320  mapdindp4  37325  mapdheq2  37331  mapdheq2biN  37332  mapdh6aN  37337  mapdh6dN  37341  mapdh6eN  37342  mapdh6hN  37345  mapdh7eN  37350  mapdh7dN  37352  mapdh7fN  37353  mapdh8ab  37379  mapdh8ad  37381  mapdh8e  37386  mapdh9a  37392  mapdh9aOLDN  37393  hdmap1l6a  37412  hdmap1l6d  37416  hdmap1l6e  37417  hdmap1l6h  37420  hdmap1eulem  37426  hdmap1eulemOLDN  37427  hdmapval0  37438  hdmapeveclem  37439  hdmapval3lemN  37442  hdmap10lem  37444  hdmap11lem1  37446  hdmaprnlem3N  37455  hdmaprnlem9N  37462  hdmaprnlem3eN  37463  imo72b2lem0  37786  imo72b2lem2  37788  imo72b2lem1  37792  imo72b2  37797
  Copyright terms: Public domain W3C validator