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

Theorem eqnetrd 2466
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 2461 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625    =/= wne 2448
This theorem is referenced by:  eqnetrrd  2468  opnz  4244  frsn  4762  onoviun  6362  intrnfi  7172  cantnfp1lem2  7383  cantnfp1lem3  7384  wemapwe  7402  acndom2  7683  fin23lem14  7961  fin23lem40  7979  isf32lem6  7986  isf34lem5  8006  isf34lem7  8007  isf34lem6  8008  axcc2lem  8064  xaddnemnf  10563  xaddnepnf  10564  fseqsupcl  11041  hashprg  11370  limsupgre  11957  isercolllem3  12142  tanval3  12416  tanneg  12430  ruclem11  12520  phibndlem  12840  dfphi2  12844  0ram  13069  0ram2  13070  ram0  13071  0ramcl  13072  gsumval2  14462  issubg2  14638  ghmrn  14698  gsumval3  15193  pgpfaclem2  15319  ablfaclem2  15323  ablfaclem3  15324  abvdom  15605  lbsextlem2  15914  gzrngunit  16439  zrngunit  16440  iinopn  16650  cnconn  17150  1stcfb  17173  fbasrn  17581  fclscmpi  17726  alexsublem  17740  dscmet  18097  reperflem  18325  evth  18459  cmetcaulem  18716  iscmet3  18721  cmetss  18742  bcthlem5  18752  bcth2  18754  mbflimsup  19023  itg1addlem4  19056  itg1climres  19071  itg2monolem1  19107  itg2i1fseq2  19113  tdeglem4  19448  deg1add  19491  deg1mul2  19502  deg1tm  19506  dgreq  19628  dgradd2  19651  dgrmul  19653  dgrmulc  19654  dgrcolem1  19656  plyrem  19687  facth  19688  fta1lem  19689  vieta1lem1  19692  vieta1lem2  19693  vieta1  19694  qaa  19705  aareccl  19708  geolim3  19721  aaliou3lem9  19732  coseq00topi  19872  cosne0  19894  tanord  19902  tanarg  19972  cxpne0  20026  cxpsqr  20052  chordthmlem  20131  chordthmlem2  20132  dcubic  20144  mcubic  20145  cubic2  20146  cubic  20147  quartlem4  20158  atandmneg  20204  atandmcj  20207  atancj  20208  atanrecl  20209  atanlogsublem  20213  efiatan2  20215  tanatan  20217  atandmtan  20218  cosatan  20219  cosatanne0  20220  wilthlem2  20309  ftalem7  20318  basellem2  20321  basellem4  20323  basellem5  20324  isppw  20354  dchrptlem2  20506  lgsne0  20574  2sqlem8a  20612  2sqlem8  20613  cntnevol  23177  xaddeq0  23306  xrge0iifhom  23321  logccne0ALT  23400  logbrec  23409  derangenlem  23704  subfacp1lem3  23715  subfacp1lem5  23717  nobndlem8  24355  itg2addnclem  24933  itg2addnclem2  24934  itg2addnc  24935  ivthALT  26269  neibastop1  26319  cmpfiiin  26783  pell1234qrne0  26949  rmxyneg  27016  bezoutr1  27084  fnwe2lem2  27159  kelac1  27172  frlmssuvc2  27258  pmtrmvd  27409  cnmsgnsubg  27445  stoweidlem23  27783  stoweidlem31  27791  wallispilem4  27828  wallispi  27830  stirlinglem3  27836  stirlinglem14  27847  elprchashprn2  28099  lsatfixedN  29272  islshpat  29280  lkrshp  29368  2llnm3N  29831  dalemdnee  29928  cdleme18b  30554  cdleme40m  30729  cdlemg12g  30911  cdlemh  31079  cdlemj3  31085  tendoconid  31091  cdlemk3  31095  cdlemk12  31112  cdlemk12u  31134  cdlemk46  31210  cdlemk54  31220  erngdvlem4  31253  erngdvlem4-rN  31261  dibn0  31416  dihglblem2aN  31556  dochshpncl  31647  dochsnnz  31713  dochsatshpb  31715  lcfl7lem  31762  lcfl8b  31767  lcfrlem33  31838  lcfr  31848  hdmaprnlem3uN  32117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278  df-ne 2450
  Copyright terms: Public domain W3C validator