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

Theorem eqnetrd 2477
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 2472 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  eqnetrrd  2479  opnz  4258  frsn  4776  onoviun  6376  intrnfi  7186  cantnfp1lem2  7397  cantnfp1lem3  7398  wemapwe  7416  acndom2  7697  fin23lem14  7975  fin23lem40  7993  isf32lem6  8000  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  axcc2lem  8078  xaddnemnf  10577  xaddnepnf  10578  fseqsupcl  11055  hashprg  11384  limsupgre  11971  isercolllem3  12156  tanval3  12430  tanneg  12444  ruclem11  12534  phibndlem  12854  dfphi2  12858  0ram  13083  0ram2  13084  ram0  13085  0ramcl  13086  gsumval2  14476  issubg2  14652  ghmrn  14712  gsumval3  15207  pgpfaclem2  15333  ablfaclem2  15337  ablfaclem3  15338  abvdom  15619  lbsextlem2  15928  gzrngunit  16453  zrngunit  16454  iinopn  16664  cnconn  17164  1stcfb  17187  fbasrn  17595  fclscmpi  17740  alexsublem  17754  dscmet  18111  reperflem  18339  evth  18473  cmetcaulem  18730  iscmet3  18735  cmetss  18756  bcthlem5  18766  bcth2  18768  mbflimsup  19037  itg1addlem4  19070  itg1climres  19085  itg2monolem1  19121  itg2i1fseq2  19127  tdeglem4  19462  deg1add  19505  deg1mul2  19516  deg1tm  19520  dgreq  19642  dgradd2  19665  dgrmul  19667  dgrmulc  19668  dgrcolem1  19670  plyrem  19701  facth  19702  fta1lem  19703  vieta1lem1  19706  vieta1lem2  19707  vieta1  19708  qaa  19719  aareccl  19722  geolim3  19735  aaliou3lem9  19746  coseq00topi  19886  cosne0  19908  tanord  19916  tanarg  19986  cxpne0  20040  cxpsqr  20066  chordthmlem  20145  chordthmlem2  20146  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  quartlem4  20172  atandmneg  20218  atandmcj  20221  atancj  20222  atanrecl  20223  atanlogsublem  20227  efiatan2  20229  tanatan  20231  atandmtan  20232  cosatan  20233  cosatanne0  20234  wilthlem2  20323  ftalem7  20332  basellem2  20335  basellem4  20337  basellem5  20338  isppw  20368  dchrptlem2  20520  lgsne0  20588  2sqlem8a  20626  2sqlem8  20627  cntnevol  23191  xaddeq0  23319  xrge0iifhom  23334  logccne0ALT  23413  logbrec  23422  derangenlem  23717  subfacp1lem3  23728  subfacp1lem5  23730  nobndlem8  24424  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  ivthALT  26361  neibastop1  26411  cmpfiiin  26875  pell1234qrne0  27041  rmxyneg  27108  bezoutr1  27176  fnwe2lem2  27251  kelac1  27264  frlmssuvc2  27350  pmtrmvd  27501  cnmsgnsubg  27537  stoweidlem23  27875  stoweidlem31  27883  wallispilem4  27920  wallispi  27922  stirlinglem3  27928  stirlinglem14  27939  elprchashprn2  28216  lsatfixedN  29821  islshpat  29829  lkrshp  29917  2llnm3N  30380  dalemdnee  30477  cdleme18b  31103  cdleme40m  31278  cdlemg12g  31460  cdlemh  31628  cdlemj3  31634  tendoconid  31640  cdlemk3  31644  cdlemk12  31661  cdlemk12u  31683  cdlemk46  31759  cdlemk54  31769  erngdvlem4  31802  erngdvlem4-rN  31810  dibn0  31965  dihglblem2aN  32105  dochshpncl  32196  dochsnnz  32262  dochsatshpb  32264  lcfl7lem  32311  lcfl8b  32316  lcfrlem33  32387  lcfr  32397  hdmaprnlem3uN  32666
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-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator