Theorem eqnetrd 2996

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  eqnetrrd  2997  3netr4d  3006  opnz  5418  xpdifid  6123  undefne0  8218  onoviun  8272  intrnfi  9311  cantnfp1lem2  9580  cantnfp1lem3  9581  wemapwe  9598  acndom2  9956  fin23lem14  10235  fin23lem40  10253  isf32lem6  10260  isf34lem5  10280  isf34lem7  10281  isf34lem6  10282  axcc2lem  10338  xaddnemnf  13142  xaddnepnf  13143  fseqsupcl  13891  hashprg  14309  elprchashprn2  14310  hash1n0  14335  limsupgre  15395  isercolllem3  15581  prodfn0  15808  ntrivcvgtail  15814  fproddiv  15875  fprodn0  15893  tanval3  16050  tanneg  16064  ruclem11  16156  nn0rppwr  16479  bezoutr1  16487  phibndlem  16688  dfphi2  16692  0ram  16939  0ram2  16940  ram0  16941  0ramcl  16942  gsumval2  18602  sgrp2nmndlem5  18845  issubg2  19062  ghmrn  19149  pmtrmvd  19376  gsumval3  19827  pgpfaclem2  20004  ablfaclem2  20008  ablfaclem3  20009  fincygsubgodd  20034  subdrgint  20727  abvdom  20754  lbsextlem2  21105  cndrng  21344  gzrngunit  21379  zringunit  21412  cnmsgnsubg  21523  frlmssuvc2  21741  mhpmulcl  22083  iinopn  22837  cnconn  23357  1stcfb  23380  dissnlocfin  23464  fbasrn  23819  fclscmpi  23964  alexsublem  23979  ustuqtop5  24180  cnextucn  24237  dscmet  24507  reperflem  24754  evth  24905  cmetcaulem  25235  iscmet3  25240  metsscmetcld  25262  cmetss  25263  bcthlem5  25275  bcth2  25277  mbflimsup  25614  itg1addlem4  25647  itg1climres  25662  itg2monolem1  25698  itg2i1fseq2  25704  tdeglem4  26012  deg1add  26055  deg1mul2  26066  deg1tm  26071  dgreq  26196  dgradd2  26221  dgrmul  26223  dgrmulc  26224  dgrcolem1  26226  plyrem  26260  facth  26261  fta1lem  26262  vieta1lem1  26265  vieta1lem2  26266  vieta1  26267  qaa  26278  aareccl  26281  geolim3  26294  aaliou3lem9  26305  coseq00topi  26458  cosne0  26485  tanord  26494  tanarg  26575  cxpne0  26633  cxpsqrt  26659  logbrec  26739  chordthmlem  26789  chordthmlem2  26790  dcubic  26803  mcubic  26804  cubic2  26805  cubic  26806  quartlem4  26817  atandmneg  26863  atandmcj  26866  atancj  26867  atanrecl  26868  atanlogsublem  26872  efiatan2  26874  tanatan  26876  atandmtan  26877  cosatan  26878  cosatanne0  26879  wilthlem2  27026  ftalem7  27036  basellem2  27039  basellem4  27041  basellem5  27042  isppw  27071  dchrptlem2  27223  lgsne0  27293  2sqlem8a  27383  2sqlem8  27384  noseponlem  27623  recsne0  28151  tglnpt2  28639  midexlem  28690  colperpexlem3  28730  mideulem2  28732  lnopp2hpgb  28761  subgruhgredgd  29283  wwlksnext  29892  wspthsnonn0vne  29916  clwwisshclwws  30016  vdn0conngrumgrv2  30197  vdgn1frgrv2  30297  nrt2irr  30474  ifnetrue  32548  ifnefals  32549  imadifxp  32602  acunirnmpt  32663  fnpreimac  32675  quad3d  32757  xaddeq0  32761  pmtrcnelor  33101  domnprodn0  33285  domnprodeq0  33286  qsidomlem2  33462  ply1dg3rt0irred  33593  m1pmeq  33594  mplmulmvr  33632  esplyind  33659  ply1annnr  33788  minplyirred  33796  rtelextdg2lem  33811  constrrtcclem  33819  constrconj  33830  constrext2chnlem  33835  constrremulcl  33852  constrrecl  33854  constrreinvcl  33857  2sqr3minply  33865  2sqr3nconstr  33866  cos9thpiminplylem1  33867  cos9thpiminplylem2  33868  cos9thpiminplylem3  33869  cos9thpiminply  33873  cos9thpinconstrlem1  33874  cos9thpinconstrlem2  33875  cos9thpinconstr  33876  madjusmdetlem2  33913  zar0ring  33963  xrge0iifhom  34022  signswn0  34645  signsvtn0  34655  signstfvneq0  34657  repr0  34696  derangenlem  35287  subfacp1lem3  35298  subfacp1lem5  35300  wsuclem  35939  ivthALT  36451  neibastop1  36475  weiunfrlem  36580  finxpreclem2  37507  finxpreclem6  37513  tan2h  37725  poimirlem9  37742  heicant  37768  itg2addnclem2  37785  lsatfixedN  39181  islshpat  39189  lkrshp  39277  2llnm3N  39741  dalemdnee  39838  cdleme18b  40464  cdleme40m  40639  cdlemg12g  40821  cdlemh  40989  cdlemj3  40995  tendoconid  41001  cdlemk3  41005  cdlemk12  41022  cdlemk12u  41044  cdlemk46  41120  cdlemk54  41130  erngdvlem4  41163  erngdvlem4-rN  41171  dibn0  41325  dihglblem2aN  41465  dochshpncl  41556  dochsnnz  41622  dochsatshpb  41624  lcfl7lem  41671  lcfl8b  41676  lcfrlem33  41747  lcfr  41757  hdmaprnlem3uN  42023  aks4d1p1p7  42240  fldhmf1  42256  primrootspoweq0  42272  idomnnzpownz  42298  idomnnzgmulnz  42299  aks6d1c5lem2  42304  deg1gprod  42306  unitscyglem4  42364  tanhalfpim  42519  remul01  42577  remulinvcom  42603  domnexpgn0cl  42693  ricdrng1  42698  prjcrv0  42791  3cubeslem2  42842  cmpfiiin  42854  pell1234qrne0  43010  rmxyneg  43077  fnwe2lem2  43208  kelac1  43220  wnefimgd  44318  radcnvrat  44471  binomcxplemfrat  44508  binomcxplemradcnv  44509  disjrnmpt2  45348  disjf1o  45351  choicefi  45360  ioondisj2  45655  ioondisj1  45656  lptioo2  45793  lptioo1  45794  0ellimcdiv  45809  liminflbuz2  45975  ioodvbdlimc1  46093  ioodvbdlimc2  46095  stoweidlem31  46191  stoweidlem59  46219  wallispilem4  46228  wallispi  46230  stirlinglem3  46236  stirlinglem14  46247  dirkerper  46256  dirkertrigeq  46261  dirkercncflem2  46264  fourierdlem4  46271  fourierdlem30  46297  fourierdlem41  46308  fourierdlem42  46309  fourierdlem44  46311  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem62  46328  fourierdlem74  46340  fourierdlem75  46341  fourierdlem79  46345  fourierdlem102  46368  fourierdlem114  46380  fouriersw  46391  elaa2lem  46393  elaa2  46394  etransclem24  46418  etransclem44  46438  etransclem47  46441  ioorrnopnlem  46464  subsaliuncl  46518  sge0cl  46541  meadjun  46622  meadjiunlem  46625  hoicvr  46708  ovnsubadd2lem  46805  smflimlem6  46936  smfpimcc  46968  smflimsuplem2  46981  cjnpoly  47051  modm2nep1  47528  modm1nep2  47530  modm1p1ne  47532  lswn0  47606  sprvalpwn0  47645  fmtnoprmfac1lem  47726  grimuhgr  48049  gpg3nbgrvtx0  48238  el0ldep  48628  islindeps2  48645  ldepsnlinclem1  48667  ldepsnlinclem2  48668  itscnhlinecirc02plem1  48944  fvconstr  49023  fvconstrn0  49024  catprs  49172  fucofvalne  49486