Theorem eqnetrd 3005

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqnetrd.2	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Assertion

Ref	Expression
eqnetrd	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Proof of Theorem eqnetrd

Step	Hyp	Ref	Expression
1		eqnetrd.2	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
2		eqnetrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	neeq1d 2997	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  eqnetrrd  3006  3netr4d  3015  opnz  5483  xpdifid  6189  undefne0  8302  onoviun  8381  intrnfi  9453  cantnfp1lem2  9716  cantnfp1lem3  9717  wemapwe  9734  acndom2  10091  fin23lem14  10370  fin23lem40  10388  isf32lem6  10395  isf34lem5  10415  isf34lem7  10416  isf34lem6  10417  axcc2lem  10473  xaddnemnf  13274  xaddnepnf  13275  fseqsupcl  14014  hashprg  14430  elprchashprn2  14431  hash1n0  14456  limsupgre  15513  isercolllem3  15699  prodfn0  15926  ntrivcvgtail  15932  fproddiv  15993  fprodn0  16011  tanval3  16166  tanneg  16180  ruclem11  16272  nn0rppwr  16594  bezoutr1  16602  phibndlem  16803  dfphi2  16807  0ram  17053  0ram2  17054  ram0  17055  0ramcl  17056  gsumval2  18711  sgrp2nmndlem5  18954  issubg2  19171  ghmrn  19259  pmtrmvd  19488  gsumval3  19939  pgpfaclem2  20116  ablfaclem2  20120  ablfaclem3  20121  fincygsubgodd  20146  subdrgint  20820  abvdom  20847  lbsextlem2  21178  cndrng  21428  gzrngunit  21468  zringunit  21494  cnmsgnsubg  21612  frlmssuvc2  21832  mhpmulcl  22170  iinopn  22923  cnconn  23445  1stcfb  23468  dissnlocfin  23552  fbasrn  23907  fclscmpi  24052  alexsublem  24067  ustuqtop5  24269  cnextucn  24327  dscmet  24600  reperflem  24853  evth  25004  cmetcaulem  25335  iscmet3  25340  metsscmetcld  25362  cmetss  25363  bcthlem5  25375  bcth2  25377  mbflimsup  25714  itg1addlem4  25747  itg1addlem4OLD  25748  itg1climres  25763  itg2monolem1  25799  itg2i1fseq2  25805  tdeglem4  26113  deg1add  26156  deg1mul2  26167  deg1tm  26172  dgreq  26297  dgradd2  26322  dgrmul  26324  dgrmulc  26325  dgrcolem1  26327  plyrem  26361  facth  26362  fta1lem  26363  vieta1lem1  26366  vieta1lem2  26367  vieta1  26368  qaa  26379  aareccl  26382  geolim3  26395  aaliou3lem9  26406  coseq00topi  26558  cosne0  26585  tanord  26594  tanarg  26675  cxpne0  26733  cxpsqrt  26759  logbrec  26839  chordthmlem  26889  chordthmlem2  26890  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  quartlem4  26917  atandmneg  26963  atandmcj  26966  atancj  26967  atanrecl  26968  atanlogsublem  26972  efiatan2  26974  tanatan  26976  atandmtan  26977  cosatan  26978  cosatanne0  26979  wilthlem2  27126  ftalem7  27136  basellem2  27139  basellem4  27141  basellem5  27142  isppw  27171  dchrptlem2  27323  lgsne0  27393  2sqlem8a  27483  2sqlem8  27484  noseponlem  27723  tglnpt2  28663  midexlem  28714  colperpexlem3  28754  mideulem2  28756  lnopp2hpgb  28785  subgruhgredgd  29315  wwlksnext  29922  wspthsnonn0vne  29946  clwwisshclwws  30043  vdn0conngrumgrv2  30224  vdgn1frgrv2  30324  nrt2irr  30501  ifnetrue  32567  ifnefals  32568  imadifxp  32620  acunirnmpt  32675  fnpreimac  32687  quad3d  32760  xaddeq0  32763  pmtrcnelor  33093  domnprodn0  33261  qsidomlem2  33460  ply1dg3rt0irred  33586  m1pmeq  33587  ply1annnr  33710  minplyirred  33718  rtelextdg2lem  33731  constrrtcclem  33739  constrconj  33749  2sqr3minply  33752  madjusmdetlem2  33788  zar0ring  33838  xrge0iifhom  33897  signswn0  34553  signsvtn0  34563  signstfvneq0  34565  repr0  34604  derangenlem  35155  subfacp1lem3  35166  subfacp1lem5  35168  wsuclem  35806  ivthALT  36317  neibastop1  36341  weiunfrlem  36446  finxpreclem2  37372  finxpreclem6  37378  tan2h  37598  poimirlem9  37615  heicant  37641  itg2addnclem2  37658  lsatfixedN  38990  islshpat  38998  lkrshp  39086  2llnm3N  39551  dalemdnee  39648  cdleme18b  40274  cdleme40m  40449  cdlemg12g  40631  cdlemh  40799  cdlemj3  40805  tendoconid  40811  cdlemk3  40815  cdlemk12  40832  cdlemk12u  40854  cdlemk46  40930  cdlemk54  40940  erngdvlem4  40973  erngdvlem4-rN  40981  dibn0  41135  dihglblem2aN  41275  dochshpncl  41366  dochsnnz  41432  dochsatshpb  41434  lcfl7lem  41481  lcfl8b  41486  lcfrlem33  41557  lcfr  41567  hdmaprnlem3uN  41833  aks4d1p1p7  42055  fldhmf1  42071  primrootspoweq0  42087  idomnnzpownz  42113  idomnnzgmulnz  42114  aks6d1c5lem2  42119  deg1gprod  42121  unitscyglem4  42179  metakunt7  42192  tanhalfpim  42363  remul01  42413  remulinvcom  42438  domnexpgn0cl  42509  ricdrng1  42514  prjcrv0  42619  3cubeslem2  42672  cmpfiiin  42684  pell1234qrne0  42840  rmxyneg  42908  fnwe2lem2  43039  kelac1  43051  wnefimgd  44150  radcnvrat  44309  binomcxplemfrat  44346  binomcxplemradcnv  44347  disjrnmpt2  45130  disjf1o  45133  choicefi  45142  ioondisj2  45445  ioondisj1  45446  lptioo2  45586  lptioo1  45587  0ellimcdiv  45604  liminflbuz2  45770  ioodvbdlimc1  45888  ioodvbdlimc2  45890  stoweidlem31  45986  stoweidlem59  46014  wallispilem4  46023  wallispi  46025  stirlinglem3  46031  stirlinglem14  46042  dirkerper  46051  dirkertrigeq  46056  dirkercncflem2  46059  fourierdlem4  46066  fourierdlem30  46092  fourierdlem41  46103  fourierdlem42  46104  fourierdlem44  46106  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem62  46123  fourierdlem74  46135  fourierdlem75  46136  fourierdlem79  46140  fourierdlem102  46163  fourierdlem114  46175  fouriersw  46186  elaa2lem  46188  elaa2  46189  etransclem24  46213  etransclem44  46233  etransclem47  46236  ioorrnopnlem  46259  subsaliuncl  46313  sge0cl  46336  meadjun  46417  meadjiunlem  46420  hoicvr  46503  ovnsubadd2lem  46600  smflimlem6  46731  smfpimcc  46763  smflimsuplem2  46776  lswn0  47368  sprvalpwn0  47407  fmtnoprmfac1lem  47488  grimuhgr  47815  gpg3nbgrvtx0  47966  el0ldep  48311  islindeps2  48328  ldepsnlinclem1  48350  ldepsnlinclem2  48351  itscnhlinecirc02plem1  48631  fvconstr  48685  fvconstrn0  48686  catprs  48799