Theorem eqnetrd 3001

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

Syntax hints:   → wi 4   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  eqnetrrd  3002  3netr4d  3011  opnz  5413  xpdifid  6119  undefne0  8219  onoviun  8273  intrnfi  9319  cantnfp1lem2  9591  cantnfp1lem3  9592  wemapwe  9609  acndom2  9967  fin23lem14  10246  fin23lem40  10264  isf32lem6  10271  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axcc2lem  10349  xaddnemnf  13179  xaddnepnf  13180  fseqsupcl  13930  hashprg  14348  elprchashprn2  14349  hash1n0  14374  limsupgre  15434  isercolllem3  15620  prodfn0  15850  ntrivcvgtail  15856  fproddiv  15917  fprodn0  15935  tanval3  16092  tanneg  16106  ruclem11  16198  nn0rppwr  16521  bezoutr1  16529  phibndlem  16731  dfphi2  16735  0ram  16982  0ram2  16983  ram0  16984  0ramcl  16985  gsumval2  18645  sgrp2nmndlem5  18891  issubg2  19108  ghmrn  19195  pmtrmvd  19422  gsumval3  19873  pgpfaclem2  20050  ablfaclem2  20054  ablfaclem3  20055  fincygsubgodd  20080  subdrgint  20775  abvdom  20802  lbsextlem2  21152  cndrng  21376  gzrngunit  21408  zringunit  21441  cnmsgnsubg  21552  frlmssuvc2  21770  mhpmulcl  22137  iinopn  22885  cnconn  23405  1stcfb  23428  dissnlocfin  23512  fbasrn  23867  fclscmpi  24012  alexsublem  24027  ustuqtop5  24228  cnextucn  24285  dscmet  24555  reperflem  24802  evth  24944  cmetcaulem  25273  iscmet3  25278  metsscmetcld  25300  cmetss  25301  bcthlem5  25313  bcth2  25315  mbflimsup  25651  itg1addlem4  25684  itg1climres  25699  itg2monolem1  25735  itg2i1fseq2  25741  tdeglem4  26043  deg1add  26086  deg1mul2  26097  deg1tm  26102  dgreq  26227  dgradd2  26251  dgrmul  26253  dgrmulc  26254  dgrcolem1  26256  plyrem  26289  facth  26290  fta1lem  26291  vieta1lem1  26294  vieta1lem2  26295  vieta1  26296  qaa  26307  aareccl  26310  geolim3  26323  aaliou3lem9  26334  coseq00topi  26484  cosne0  26511  tanord  26520  tanarg  26601  cxpne0  26659  cxpsqrt  26685  logbrec  26764  chordthmlem  26814  chordthmlem2  26815  dcubic  26828  mcubic  26829  cubic2  26830  cubic  26831  quartlem4  26842  atandmneg  26888  atandmcj  26891  atancj  26892  atanrecl  26893  atanlogsublem  26897  efiatan2  26899  tanatan  26901  atandmtan  26902  cosatan  26903  cosatanne0  26904  wilthlem2  27050  ftalem7  27060  basellem2  27063  basellem4  27065  basellem5  27066  isppw  27095  dchrptlem2  27246  lgsne0  27316  2sqlem8a  27406  2sqlem8  27407  noseponlem  27646  recsne0  28202  tglnpt2  28727  midexlem  28778  colperpexlem3  28818  mideulem2  28820  lnopp2hpgb  28849  subgruhgredgd  29371  wwlksnext  29979  wspthsnonn0vne  30003  clwwisshclwws  30103  vdn0conngrumgrv2  30284  vdgn1frgrv2  30384  nrt2irr  30561  ifnetrue  32635  ifnefals  32636  imadifxp  32690  acunirnmpt  32751  fnpreimac  32762  quad3d  32841  xaddeq0  32845  pmtrcnelor  33172  domnprodn0  33356  domnprodeq0  33357  qsidomlem2  33536  ply1dg3rt0irred  33667  m1pmeq  33668  mplmulmvr  33723  esplyfvaln  33758  esplyind  33759  ply1annnr  33887  minplyirred  33895  rtelextdg2lem  33910  constrrtcclem  33918  constrconj  33929  constrext2chnlem  33934  constrremulcl  33951  constrrecl  33953  constrreinvcl  33956  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpiminplylem1  33966  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminply  33972  cos9thpinconstrlem1  33973  cos9thpinconstrlem2  33974  cos9thpinconstr  33975  madjusmdetlem2  34012  zar0ring  34062  xrge0iifhom  34121  signswn0  34744  signsvtn0  34754  signstfvneq0  34756  repr0  34795  derangenlem  35399  subfacp1lem3  35410  subfacp1lem5  35412  wsuclem  36051  ivthALT  36563  neibastop1  36587  weiunfrlem  36692  finxpreclem2  37752  finxpreclem6  37758  tan2h  37979  poimirlem9  37996  heicant  38022  itg2addnclem2  38039  lsatfixedN  39501  islshpat  39509  lkrshp  39597  2llnm3N  40061  dalemdnee  40158  cdleme18b  40784  cdleme40m  40959  cdlemg12g  41141  cdlemh  41309  cdlemj3  41315  tendoconid  41321  cdlemk3  41325  cdlemk12  41342  cdlemk12u  41364  cdlemk46  41440  cdlemk54  41450  erngdvlem4  41483  erngdvlem4-rN  41491  dibn0  41645  dihglblem2aN  41785  dochshpncl  41876  dochsnnz  41942  dochsatshpb  41944  lcfl7lem  41991  lcfl8b  41996  lcfrlem33  42067  lcfr  42077  hdmaprnlem3uN  42343  aks4d1p1p7  42559  fldhmf1  42575  primrootspoweq0  42591  idomnnzpownz  42617  idomnnzgmulnz  42618  aks6d1c5lem2  42623  deg1gprod  42625  unitscyglem4  42683  tanhalfpim  42826  remul01  42884  remulinvcom  42910  domnexpgn0cl  43009  ricdrng1  43014  prjcrv0  43083  3cubeslem2  43134  cmpfiiin  43146  pell1234qrne0  43298  rmxyneg  43365  fnwe2lem2  43496  kelac1  43508  wnefimgd  44605  radcnvrat  44758  binomcxplemfrat  44795  binomcxplemradcnv  44796  disjrnmpt2  45635  disjf1o  45638  choicefi  45646  ioondisj2  45938  ioondisj1  45939  lptioo2  46076  lptioo1  46077  0ellimcdiv  46092  liminflbuz2  46258  ioodvbdlimc1  46376  ioodvbdlimc2  46378  stoweidlem31  46474  stoweidlem59  46502  wallispilem4  46511  wallispi  46513  stirlinglem3  46519  stirlinglem14  46530  dirkerper  46539  dirkertrigeq  46544  dirkercncflem2  46547  fourierdlem4  46554  fourierdlem30  46580  fourierdlem41  46591  fourierdlem42  46592  fourierdlem44  46594  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem74  46623  fourierdlem75  46624  fourierdlem79  46628  fourierdlem102  46651  fourierdlem114  46663  fouriersw  46674  elaa2lem  46676  elaa2  46677  etransclem24  46701  etransclem44  46721  etransclem47  46724  ioorrnopnlem  46747  subsaliuncl  46801  sge0cl  46824  meadjun  46905  meadjiunlem  46908  hoicvr  46991  ovnsubadd2lem  47088  smflimlem6  47219  smfpimcc  47251  smflimsuplem2  47264  cjnpoly  47352  modm2nep1  47835  modm1nep2  47837  modm1p1ne  47839  lswn0  47919  sprvalpwn0  47958  fmtnoprmfac1lem  48042  grimuhgr  48378  gpg3nbgrvtx0  48567  el0ldep  48957  islindeps2  48974  ldepsnlinclem1  48996  ldepsnlinclem2  48997  itscnhlinecirc02plem1  49273  fvconstr  49352  fvconstrn0  49353  catprs  49501  fucofvalne  49815