Theorem eqnetrd 3008

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 3000	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))
4	1, 3	mpbird 257	1 ⊢ (𝜑 → 𝐴 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  eqnetrrd  3009  3netr4d  3018  opnz  5478  xpdifid  6188  undefne0  8304  onoviun  8383  intrnfi  9456  cantnfp1lem2  9719  cantnfp1lem3  9720  wemapwe  9737  acndom2  10094  fin23lem14  10373  fin23lem40  10391  isf32lem6  10398  isf34lem5  10418  isf34lem7  10419  isf34lem6  10420  axcc2lem  10476  xaddnemnf  13278  xaddnepnf  13279  fseqsupcl  14018  hashprg  14434  elprchashprn2  14435  hash1n0  14460  limsupgre  15517  isercolllem3  15703  prodfn0  15930  ntrivcvgtail  15936  fproddiv  15997  fprodn0  16015  tanval3  16170  tanneg  16184  ruclem11  16276  nn0rppwr  16598  bezoutr1  16606  phibndlem  16807  dfphi2  16811  0ram  17058  0ram2  17059  ram0  17060  0ramcl  17061  gsumval2  18699  sgrp2nmndlem5  18942  issubg2  19159  ghmrn  19247  pmtrmvd  19474  gsumval3  19925  pgpfaclem2  20102  ablfaclem2  20106  ablfaclem3  20107  fincygsubgodd  20132  subdrgint  20804  abvdom  20831  lbsextlem2  21161  cndrng  21411  gzrngunit  21451  zringunit  21477  cnmsgnsubg  21595  frlmssuvc2  21815  mhpmulcl  22153  iinopn  22908  cnconn  23430  1stcfb  23453  dissnlocfin  23537  fbasrn  23892  fclscmpi  24037  alexsublem  24052  ustuqtop5  24254  cnextucn  24312  dscmet  24585  reperflem  24840  evth  24991  cmetcaulem  25322  iscmet3  25327  metsscmetcld  25349  cmetss  25350  bcthlem5  25362  bcth2  25364  mbflimsup  25701  itg1addlem4  25734  itg1climres  25749  itg2monolem1  25785  itg2i1fseq2  25791  tdeglem4  26099  deg1add  26142  deg1mul2  26153  deg1tm  26158  dgreq  26283  dgradd2  26308  dgrmul  26310  dgrmulc  26311  dgrcolem1  26313  plyrem  26347  facth  26348  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  vieta1  26354  qaa  26365  aareccl  26368  geolim3  26381  aaliou3lem9  26392  coseq00topi  26544  cosne0  26571  tanord  26580  tanarg  26661  cxpne0  26719  cxpsqrt  26745  logbrec  26825  chordthmlem  26875  chordthmlem2  26876  dcubic  26889  mcubic  26890  cubic2  26891  cubic  26892  quartlem4  26903  atandmneg  26949  atandmcj  26952  atancj  26953  atanrecl  26954  atanlogsublem  26958  efiatan2  26960  tanatan  26962  atandmtan  26963  cosatan  26964  cosatanne0  26965  wilthlem2  27112  ftalem7  27122  basellem2  27125  basellem4  27127  basellem5  27128  isppw  27157  dchrptlem2  27309  lgsne0  27379  2sqlem8a  27469  2sqlem8  27470  noseponlem  27709  tglnpt2  28649  midexlem  28700  colperpexlem3  28740  mideulem2  28742  lnopp2hpgb  28771  subgruhgredgd  29301  wwlksnext  29913  wspthsnonn0vne  29937  clwwisshclwws  30034  vdn0conngrumgrv2  30215  vdgn1frgrv2  30315  nrt2irr  30492  ifnetrue  32560  ifnefals  32561  imadifxp  32614  acunirnmpt  32669  fnpreimac  32681  quad3d  32754  xaddeq0  32757  pmtrcnelor  33111  domnprodn0  33279  qsidomlem2  33481  ply1dg3rt0irred  33607  m1pmeq  33608  ply1annnr  33746  minplyirred  33754  rtelextdg2lem  33767  constrrtcclem  33775  constrconj  33786  2sqr3minply  33791  madjusmdetlem2  33827  zar0ring  33877  xrge0iifhom  33936  signswn0  34575  signsvtn0  34585  signstfvneq0  34587  repr0  34626  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  wsuclem  35826  ivthALT  36336  neibastop1  36360  weiunfrlem  36465  finxpreclem2  37391  finxpreclem6  37397  tan2h  37619  poimirlem9  37636  heicant  37662  itg2addnclem2  37679  lsatfixedN  39010  islshpat  39018  lkrshp  39106  2llnm3N  39571  dalemdnee  39668  cdleme18b  40294  cdleme40m  40469  cdlemg12g  40651  cdlemh  40819  cdlemj3  40825  tendoconid  40831  cdlemk3  40835  cdlemk12  40852  cdlemk12u  40874  cdlemk46  40950  cdlemk54  40960  erngdvlem4  40993  erngdvlem4-rN  41001  dibn0  41155  dihglblem2aN  41295  dochshpncl  41386  dochsnnz  41452  dochsatshpb  41454  lcfl7lem  41501  lcfl8b  41506  lcfrlem33  41577  lcfr  41587  hdmaprnlem3uN  41853  aks4d1p1p7  42075  fldhmf1  42091  primrootspoweq0  42107  idomnnzpownz  42133  idomnnzgmulnz  42134  aks6d1c5lem2  42139  deg1gprod  42141  unitscyglem4  42199  metakunt7  42212  tanhalfpim  42385  remul01  42437  remulinvcom  42462  domnexpgn0cl  42533  ricdrng1  42538  prjcrv0  42643  3cubeslem2  42696  cmpfiiin  42708  pell1234qrne0  42864  rmxyneg  42932  fnwe2lem2  43063  kelac1  43075  wnefimgd  44174  radcnvrat  44333  binomcxplemfrat  44370  binomcxplemradcnv  44371  disjrnmpt2  45193  disjf1o  45196  choicefi  45205  ioondisj2  45506  ioondisj1  45507  lptioo2  45646  lptioo1  45647  0ellimcdiv  45664  liminflbuz2  45830  ioodvbdlimc1  45948  ioodvbdlimc2  45950  stoweidlem31  46046  stoweidlem59  46074  wallispilem4  46083  wallispi  46085  stirlinglem3  46091  stirlinglem14  46102  dirkerper  46111  dirkertrigeq  46116  dirkercncflem2  46119  fourierdlem4  46126  fourierdlem30  46152  fourierdlem41  46163  fourierdlem42  46164  fourierdlem44  46166  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem74  46195  fourierdlem75  46196  fourierdlem79  46200  fourierdlem102  46223  fourierdlem114  46235  fouriersw  46246  elaa2lem  46248  elaa2  46249  etransclem24  46273  etransclem44  46293  etransclem47  46296  ioorrnopnlem  46319  subsaliuncl  46373  sge0cl  46396  meadjun  46477  meadjiunlem  46480  hoicvr  46563  ovnsubadd2lem  46660  smflimlem6  46791  smfpimcc  46823  smflimsuplem2  46836  lswn0  47431  sprvalpwn0  47470  fmtnoprmfac1lem  47551  grimuhgr  47878  gpg3nbgrvtx0  48032  el0ldep  48383  islindeps2  48400  ldepsnlinclem1  48422  ldepsnlinclem2  48423  itscnhlinecirc02plem1  48703  fvconstr  48765  fvconstrn0  48766  catprs  48900  fucofvalne  49020