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

Theorem eqnetrd 2616
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetrd.1  |-  ( ph  ->  A  =  B )
eqnetrd.2  |-  ( ph  ->  B  =/=  C )
Assertion
Ref Expression
eqnetrd  |-  ( ph  ->  A  =/=  C )

Proof of Theorem eqnetrd
StepHypRef Expression
1 eqnetrd.2 . 2  |-  ( ph  ->  B  =/=  C )
2 eqnetrd.1 . . 3  |-  ( ph  ->  A  =  B )
32neeq1d 2611 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 224 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    =/= wne 2598
This theorem is referenced by:  eqnetrrd  2618  opnz  4424  frsn  4940  xpimasn  5308  onoviun  6597  intrnfi  7413  cantnfp1lem2  7627  cantnfp1lem3  7628  wemapwe  7646  acndom2  7927  fin23lem14  8205  fin23lem40  8223  isf32lem6  8230  isf34lem5  8250  isf34lem7  8251  isf34lem6  8252  axcc2lem  8308  xaddnemnf  10812  xaddnepnf  10813  fseqsupcl  11308  hashprg  11658  elprchashprn2  11659  limsupgre  12267  isercolllem3  12452  tanval3  12727  tanneg  12741  ruclem11  12831  phibndlem  13151  dfphi2  13155  0ram  13380  0ram2  13381  ram0  13382  0ramcl  13383  gsumval2  14775  issubg2  14951  ghmrn  15011  gsumval3  15506  pgpfaclem2  15632  ablfaclem2  15636  ablfaclem3  15637  abvdom  15918  lbsextlem2  16223  gzrngunit  16756  zrngunit  16757  iinopn  16967  cnconn  17477  1stcfb  17500  fbasrn  17908  fclscmpi  18053  alexsublem  18067  ustuqtop5  18267  cnextucn  18325  dscmet  18612  reperflem  18841  evth  18976  cmetcaulem  19233  iscmet3  19238  cmetss  19259  bcthlem5  19273  bcth2  19275  mbflimsup  19550  itg1addlem4  19583  itg1climres  19598  itg2monolem1  19634  itg2i1fseq2  19640  tdeglem4  19975  deg1add  20018  deg1mul2  20029  deg1tm  20033  dgreq  20155  dgradd2  20178  dgrmul  20180  dgrmulc  20181  dgrcolem1  20183  plyrem  20214  facth  20215  fta1lem  20216  vieta1lem1  20219  vieta1lem2  20220  vieta1  20221  qaa  20232  aareccl  20235  geolim3  20248  aaliou3lem9  20259  coseq00topi  20402  cosne0  20424  tanord  20432  tanarg  20506  cxpne0  20560  cxpsqr  20586  chordthmlem  20665  chordthmlem2  20666  dcubic  20678  mcubic  20679  cubic2  20680  cubic  20681  quartlem4  20692  atandmneg  20738  atandmcj  20741  atancj  20742  atanrecl  20743  atanlogsublem  20747  efiatan2  20749  tanatan  20751  atandmtan  20752  cosatan  20753  cosatanne0  20754  wilthlem2  20844  ftalem7  20853  basellem2  20856  basellem4  20858  basellem5  20859  isppw  20889  dchrptlem2  21041  lgsne0  21109  2sqlem8a  21147  2sqlem8  21148  imadifxp  24030  xaddeq0  24111  xrge0iifhom  24315  logccne0OLD  24387  logbrec  24397  derangenlem  24849  subfacp1lem3  24860  subfacp1lem5  24862  prodfn0  25214  ntrivcvgtail  25220  fproddiv  25277  fprodn0  25295  wsuclem  25568  nobndlem8  25646  itg2addnclem2  26247  ivthALT  26329  neibastop1  26379  cmpfiiin  26742  pell1234qrne0  26907  rmxyneg  26974  bezoutr1  27042  fnwe2lem2  27117  kelac1  27129  frlmssuvc2  27215  pmtrmvd  27366  cnmsgnsubg  27402  stoweidlem31  27747  stoweidlem59  27775  wallispilem4  27784  wallispi  27786  stirlinglem3  27792  stirlinglem14  27803  lswrdn0  28226  cshwssizelem1a  28242  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  lsatfixedN  29744  islshpat  29752  lkrshp  29840  2llnm3N  30303  dalemdnee  30400  cdleme18b  31026  cdleme40m  31201  cdlemg12g  31383  cdlemh  31551  cdlemj3  31557  tendoconid  31563  cdlemk3  31567  cdlemk12  31584  cdlemk12u  31606  cdlemk46  31682  cdlemk54  31692  erngdvlem4  31725  erngdvlem4-rN  31733  dibn0  31888  dihglblem2aN  32028  dochshpncl  32119  dochsnnz  32185  dochsatshpb  32187  lcfl7lem  32234  lcfl8b  32239  lcfrlem33  32310  lcfr  32320  hdmaprnlem3uN  32589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428  df-ne 2600
  Copyright terms: Public domain W3C validator