Theorem eqnetrd 3000

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  eqnetrrd  3001  3netr4d  3010  opnz  5429  xpdifid  6134  undefne0  8231  onoviun  8285  intrnfi  9331  cantnfp1lem2  9600  cantnfp1lem3  9601  wemapwe  9618  acndom2  9976  fin23lem14  10255  fin23lem40  10273  isf32lem6  10280  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axcc2lem  10358  xaddnemnf  13163  xaddnepnf  13164  fseqsupcl  13912  hashprg  14330  elprchashprn2  14331  hash1n0  14356  limsupgre  15416  isercolllem3  15602  prodfn0  15829  ntrivcvgtail  15835  fproddiv  15896  fprodn0  15914  tanval3  16071  tanneg  16085  ruclem11  16177  nn0rppwr  16500  bezoutr1  16508  phibndlem  16709  dfphi2  16713  0ram  16960  0ram2  16961  ram0  16962  0ramcl  16963  gsumval2  18623  sgrp2nmndlem5  18866  issubg2  19083  ghmrn  19170  pmtrmvd  19397  gsumval3  19848  pgpfaclem2  20025  ablfaclem2  20029  ablfaclem3  20030  fincygsubgodd  20055  subdrgint  20748  abvdom  20775  lbsextlem2  21126  cndrng  21365  gzrngunit  21400  zringunit  21433  cnmsgnsubg  21544  frlmssuvc2  21762  mhpmulcl  22104  iinopn  22858  cnconn  23378  1stcfb  23401  dissnlocfin  23485  fbasrn  23840  fclscmpi  23985  alexsublem  24000  ustuqtop5  24201  cnextucn  24258  dscmet  24528  reperflem  24775  evth  24926  cmetcaulem  25256  iscmet3  25261  metsscmetcld  25283  cmetss  25284  bcthlem5  25296  bcth2  25298  mbflimsup  25635  itg1addlem4  25668  itg1climres  25683  itg2monolem1  25719  itg2i1fseq2  25725  tdeglem4  26033  deg1add  26076  deg1mul2  26087  deg1tm  26092  dgreq  26217  dgradd2  26242  dgrmul  26244  dgrmulc  26245  dgrcolem1  26247  plyrem  26281  facth  26282  fta1lem  26283  vieta1lem1  26286  vieta1lem2  26287  vieta1  26288  qaa  26299  aareccl  26302  geolim3  26315  aaliou3lem9  26326  coseq00topi  26479  cosne0  26506  tanord  26515  tanarg  26596  cxpne0  26654  cxpsqrt  26680  logbrec  26760  chordthmlem  26810  chordthmlem2  26811  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  quartlem4  26838  atandmneg  26884  atandmcj  26887  atancj  26888  atanrecl  26889  atanlogsublem  26893  efiatan2  26895  tanatan  26897  atandmtan  26898  cosatan  26899  cosatanne0  26900  wilthlem2  27047  ftalem7  27057  basellem2  27060  basellem4  27062  basellem5  27063  isppw  27092  dchrptlem2  27244  lgsne0  27314  2sqlem8a  27404  2sqlem8  27405  noseponlem  27644  recsne0  28200  tglnpt2  28725  midexlem  28776  colperpexlem3  28816  mideulem2  28818  lnopp2hpgb  28847  subgruhgredgd  29369  wwlksnext  29978  wspthsnonn0vne  30002  clwwisshclwws  30102  vdn0conngrumgrv2  30283  vdgn1frgrv2  30383  nrt2irr  30560  ifnetrue  32634  ifnefals  32635  imadifxp  32688  acunirnmpt  32749  fnpreimac  32760  quad3d  32840  xaddeq0  32844  pmtrcnelor  33185  domnprodn0  33369  domnprodeq0  33370  qsidomlem2  33546  ply1dg3rt0irred  33677  m1pmeq  33678  mplmulmvr  33716  esplyfvaln  33751  esplyind  33752  ply1annnr  33881  minplyirred  33889  rtelextdg2lem  33904  constrrtcclem  33912  constrconj  33923  constrext2chnlem  33928  constrremulcl  33945  constrrecl  33947  constrreinvcl  33950  2sqr3minply  33958  2sqr3nconstr  33959  cos9thpiminplylem1  33960  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  cos9thpiminply  33966  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  cos9thpinconstr  33969  madjusmdetlem2  34006  zar0ring  34056  xrge0iifhom  34115  signswn0  34738  signsvtn0  34748  signstfvneq0  34750  repr0  34789  derangenlem  35387  subfacp1lem3  35398  subfacp1lem5  35400  wsuclem  36039  ivthALT  36551  neibastop1  36575  weiunfrlem  36680  finxpreclem2  37645  finxpreclem6  37651  tan2h  37863  poimirlem9  37880  heicant  37906  itg2addnclem2  37923  lsatfixedN  39385  islshpat  39393  lkrshp  39481  2llnm3N  39945  dalemdnee  40042  cdleme18b  40668  cdleme40m  40843  cdlemg12g  41025  cdlemh  41193  cdlemj3  41199  tendoconid  41205  cdlemk3  41209  cdlemk12  41226  cdlemk12u  41248  cdlemk46  41324  cdlemk54  41334  erngdvlem4  41367  erngdvlem4-rN  41375  dibn0  41529  dihglblem2aN  41669  dochshpncl  41760  dochsnnz  41826  dochsatshpb  41828  lcfl7lem  41875  lcfl8b  41880  lcfrlem33  41951  lcfr  41961  hdmaprnlem3uN  42227  aks4d1p1p7  42444  fldhmf1  42460  primrootspoweq0  42476  idomnnzpownz  42502  idomnnzgmulnz  42503  aks6d1c5lem2  42508  deg1gprod  42510  unitscyglem4  42568  tanhalfpim  42719  remul01  42777  remulinvcom  42803  domnexpgn0cl  42893  ricdrng1  42898  prjcrv0  42991  3cubeslem2  43042  cmpfiiin  43054  pell1234qrne0  43210  rmxyneg  43277  fnwe2lem2  43408  kelac1  43420  wnefimgd  44517  radcnvrat  44670  binomcxplemfrat  44707  binomcxplemradcnv  44708  disjrnmpt2  45547  disjf1o  45550  choicefi  45558  ioondisj2  45853  ioondisj1  45854  lptioo2  45991  lptioo1  45992  0ellimcdiv  46007  liminflbuz2  46173  ioodvbdlimc1  46291  ioodvbdlimc2  46293  stoweidlem31  46389  stoweidlem59  46417  wallispilem4  46426  wallispi  46428  stirlinglem3  46434  stirlinglem14  46445  dirkerper  46454  dirkertrigeq  46459  dirkercncflem2  46462  fourierdlem4  46469  fourierdlem30  46495  fourierdlem41  46506  fourierdlem42  46507  fourierdlem44  46509  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem62  46526  fourierdlem74  46538  fourierdlem75  46539  fourierdlem79  46543  fourierdlem102  46566  fourierdlem114  46578  fouriersw  46589  elaa2lem  46591  elaa2  46592  etransclem24  46616  etransclem44  46636  etransclem47  46639  ioorrnopnlem  46662  subsaliuncl  46716  sge0cl  46739  meadjun  46820  meadjiunlem  46823  hoicvr  46906  ovnsubadd2lem  47003  smflimlem6  47134  smfpimcc  47166  smflimsuplem2  47179  cjnpoly  47249  modm2nep1  47726  modm1nep2  47728  modm1p1ne  47730  lswn0  47804  sprvalpwn0  47843  fmtnoprmfac1lem  47924  grimuhgr  48247  gpg3nbgrvtx0  48436  el0ldep  48826  islindeps2  48843  ldepsnlinclem1  48865  ldepsnlinclem2  48866  itscnhlinecirc02plem1  49142  fvconstr  49221  fvconstrn0  49222  catprs  49370  fucofvalne  49684