Theorem eqnetrd 3023

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

Syntax hints:   → wi 4   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  eqnetrrd  3024  3netr4d  3033  opnz  5438  xpdifid  6149  undefne0  8254  onoviun  8308  intrnfi  9356  cantnfp1lem2  9628  cantnfp1lem3  9629  wemapwe  9646  acndom2  10004  fin23lem14  10284  fin23lem40  10302  isf32lem6  10309  isf34lem5  10329  isf34lem7  10330  isf34lem6  10331  axcc2lem  10387  xaddnemnf  13233  xaddnepnf  13234  fseqsupcl  13984  hashprg  14402  elprchashprn2  14403  hash1n0  14428  limsupgre  15499  isercolllem3  15685  prodfn0  15915  ntrivcvgtail  15921  fproddiv  15982  fprodn0  16000  tanval3  16157  tanneg  16171  ruclem11  16263  nn0rppwr  16586  bezoutr1  16594  phibndlem  16796  dfphi2  16800  0ram  17047  0ram2  17048  ram0  17049  0ramcl  17050  gsumval2  18711  sgrp2nmndlem5  18957  issubg2  19174  ghmrn  19260  pmtrmvd  19487  gsumval3  19938  pgpfaclem2  20115  ablfaclem2  20119  ablfaclem3  20120  fincygsubgodd  20145  subdrgint  20840  abvdom  20867  lbsextlem2  21217  cndrng  21441  gzrngunit  21473  zringunit  21506  cnmsgnsubg  21617  frlmssuvc2  21835  mhpmulcl  22202  iinopn  22950  cnconn  23470  1stcfb  23493  dissnlocfin  23577  fbasrn  23932  fclscmpi  24077  alexsublem  24092  ustuqtop5  24293  cnextucn  24350  dscmet  24620  reperflem  24867  evth  25009  cmetcaulem  25338  iscmet3  25343  metsscmetcld  25365  cmetss  25366  bcthlem5  25378  bcth2  25380  mbflimsup  25716  itg1addlem4  25749  itg1climres  25764  itg2monolem1  25800  itg2i1fseq2  25806  tdeglem4  26108  deg1add  26151  deg1mul2  26162  deg1tm  26167  dgreq  26292  dgradd2  26316  dgrmul  26318  dgrmulc  26319  dgrcolem1  26321  plyrem  26357  facth  26358  fta1lem  26359  vieta1lem1  26362  vieta1lem2  26363  vieta1  26364  qaa  26375  aareccl  26378  geolim3  26391  aaliou3lem9  26402  coseq00topi  26555  cosne0  26582  tanord  26591  tanarg  26672  cxpne0  26730  cxpsqrt  26756  logbrec  26835  chordthmlem  26885  chordthmlem2  26886  dcubic  26899  mcubic  26900  cubic2  26901  cubic  26902  quartlem4  26913  atandmneg  26959  atandmcj  26962  atancj  26963  atanrecl  26964  atanlogsublem  26968  efiatan2  26970  tanatan  26972  atandmtan  26973  cosatan  26974  cosatanne0  26975  wilthlem2  27121  ftalem7  27131  basellem2  27134  basellem4  27136  basellem5  27137  isppw  27166  dchrptlem2  27317  lgsne0  27387  2sqlem8a  27477  2sqlem8  27478  noseponlem  27716  recsne0  28273  tglnpt2  28798  midexlem  28849  colperpexlem3  28889  mideulem2  28891  lnopp2hpgb  28920  subgruhgredgd  29442  wwlksnext  30050  wspthsnonn0vne  30074  clwwisshclwws  30174  vdn0conngrumgrv2  30355  vdgn1frgrv2  30455  nrt2irr  30632  ifnetrue  32706  ifnefals  32707  imadifxp  32761  acunirnmpt  32822  fnpreimac  32833  quad3d  32912  xaddeq0  32916  pmtrcnelor  33232  domnprodn0  33420  domnprodeq0  33421  qsidomlem2  33601  drnglring  33649  dflringlem3  33653  dflring4  33655  ply1dg3rt0irred  33741  m1pmeq  33742  mplmulmvr  33797  esplyfvaln  33832  esplyind  33833  ply1annnr  33961  minplyirred  33969  rtelextdg2lem  33984  constrrtcclem  33992  constrconj  34003  constrext2chnlem  34008  constrremulcl  34025  constrrecl  34027  constrreinvcl  34030  2sqr3minply  34038  2sqr3nconstr  34039  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  cos9thpiminplylem3  34042  cos9thpiminply  34046  cos9thpinconstrlem1  34047  cos9thpinconstrlem2  34048  cos9thpinconstr  34049  madjusmdetlem2  34086  zar0ring  34136  xrge0iifhom  34195  signswn0  34815  signsvtn0  34825  signstfvneq0  34827  repr0  34866  derangenlem  35482  subfacp1lem3  35493  subfacp1lem5  35495  wsuclem  36134  ivthALT  36656  neibastop1  36680  weiunfrlem  36785  finxpreclem2  37845  finxpreclem6  37851  tan2h  38072  poimirlem9  38089  heicant  38115  itg2addnclem2  38132  lsatfixedN  39594  islshpat  39602  lkrshp  39690  2llnm3N  40154  dalemdnee  40251  cdleme18b  40877  cdleme40m  41052  cdlemg12g  41234  cdlemh  41402  cdlemj3  41408  tendoconid  41414  cdlemk3  41418  cdlemk12  41435  cdlemk12u  41457  cdlemk46  41533  cdlemk54  41543  erngdvlem4  41576  erngdvlem4-rN  41584  dibn0  41738  dihglblem2aN  41878  dochshpncl  41969  dochsnnz  42035  dochsatshpb  42037  lcfl7lem  42084  lcfl8b  42089  lcfrlem33  42160  lcfr  42170  hdmaprnlem3uN  42436  aks4d1p1p7  42652  fldhmf1  42668  primrootspoweq0  42684  idomnnzpownz  42710  idomnnzgmulnz  42711  aks6d1c5lem2  42716  deg1gprod  42718  unitscyglem4  42776  tanhalfpim  42919  remul01  42977  remulinvcom  43003  domnexpgn0cl  43102  ricdrng1  43107  prjcrv0  43176  3cubeslem2  43227  cmpfiiin  43239  pell1234qrne0  43391  rmxyneg  43458  fnwe2lem2  43589  kelac1  43601  wnefimgd  44698  radcnvrat  44851  binomcxplemfrat  44888  binomcxplemradcnv  44889  disjrnmpt2  45727  disjf1o  45730  choicefi  45738  ioondisj2  46030  ioondisj1  46031  lptioo2  46168  lptioo1  46169  0ellimcdiv  46184  liminflbuz2  46350  ioodvbdlimc1  46468  ioodvbdlimc2  46470  stoweidlem31  46566  stoweidlem59  46594  wallispilem4  46603  wallispi  46605  stirlinglem3  46611  stirlinglem14  46622  dirkerper  46631  dirkertrigeq  46636  dirkercncflem2  46639  fourierdlem4  46646  fourierdlem30  46672  fourierdlem41  46683  fourierdlem42  46684  fourierdlem44  46686  fourierdlem46  46687  fourierdlem48  46689  fourierdlem49  46690  fourierdlem62  46703  fourierdlem74  46715  fourierdlem75  46716  fourierdlem79  46720  fourierdlem102  46743  fourierdlem114  46755  fouriersw  46766  elaa2lem  46768  elaa2  46769  etransclem24  46793  etransclem44  46813  etransclem47  46816  ioorrnopnlem  46839  subsaliuncl  46893  sge0cl  46916  meadjun  46997  meadjiunlem  47000  hoicvr  47083  ovnsubadd2lem  47180  smflimlem6  47311  smfpimcc  47343  smflimsuplem2  47356  cjnpoly  47444  modm2nep1  47927  modm1nep2  47929  modm1p1ne  47931  lswn0  48011  sprvalpwn0  48050  fmtnoprmfac1lem  48134  grimuhgr  48470  gpg3nbgrvtx0  48659  el0ldep  49049  islindeps2  49066  ldepsnlinclem1  49088  ldepsnlinclem2  49089  itscnhlinecirc02plem1  49365  fvconstr  49444  fvconstrn0  49445  catprs  49593  fucofvalne  49907