Theorem eqnetrd 2999

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

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

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 2708

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

This theorem is referenced by:  eqnetrrd  3000  3netr4d  3009  opnz  5421  xpdifid  6126  undefne0  8221  onoviun  8275  intrnfi  9319  cantnfp1lem2  9588  cantnfp1lem3  9589  wemapwe  9606  acndom2  9964  fin23lem14  10243  fin23lem40  10261  isf32lem6  10268  isf34lem5  10288  isf34lem7  10289  isf34lem6  10290  axcc2lem  10346  xaddnemnf  13151  xaddnepnf  13152  fseqsupcl  13900  hashprg  14318  elprchashprn2  14319  hash1n0  14344  limsupgre  15404  isercolllem3  15590  prodfn0  15817  ntrivcvgtail  15823  fproddiv  15884  fprodn0  15902  tanval3  16059  tanneg  16073  ruclem11  16165  nn0rppwr  16488  bezoutr1  16496  phibndlem  16697  dfphi2  16701  0ram  16948  0ram2  16949  ram0  16950  0ramcl  16951  gsumval2  18611  sgrp2nmndlem5  18854  issubg2  19071  ghmrn  19158  pmtrmvd  19385  gsumval3  19836  pgpfaclem2  20013  ablfaclem2  20017  ablfaclem3  20018  fincygsubgodd  20043  subdrgint  20736  abvdom  20763  lbsextlem2  21114  cndrng  21353  gzrngunit  21388  zringunit  21421  cnmsgnsubg  21532  frlmssuvc2  21750  mhpmulcl  22092  iinopn  22846  cnconn  23366  1stcfb  23389  dissnlocfin  23473  fbasrn  23828  fclscmpi  23973  alexsublem  23988  ustuqtop5  24189  cnextucn  24246  dscmet  24516  reperflem  24763  evth  24914  cmetcaulem  25244  iscmet3  25249  metsscmetcld  25271  cmetss  25272  bcthlem5  25284  bcth2  25286  mbflimsup  25623  itg1addlem4  25656  itg1climres  25671  itg2monolem1  25707  itg2i1fseq2  25713  tdeglem4  26021  deg1add  26064  deg1mul2  26075  deg1tm  26080  dgreq  26205  dgradd2  26230  dgrmul  26232  dgrmulc  26233  dgrcolem1  26235  plyrem  26269  facth  26270  fta1lem  26271  vieta1lem1  26274  vieta1lem2  26275  vieta1  26276  qaa  26287  aareccl  26290  geolim3  26303  aaliou3lem9  26314  coseq00topi  26467  cosne0  26494  tanord  26503  tanarg  26584  cxpne0  26642  cxpsqrt  26668  logbrec  26748  chordthmlem  26798  chordthmlem2  26799  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  quartlem4  26826  atandmneg  26872  atandmcj  26875  atancj  26876  atanrecl  26877  atanlogsublem  26881  efiatan2  26883  tanatan  26885  atandmtan  26886  cosatan  26887  cosatanne0  26888  wilthlem2  27035  ftalem7  27045  basellem2  27048  basellem4  27050  basellem5  27051  isppw  27080  dchrptlem2  27232  lgsne0  27302  2sqlem8a  27392  2sqlem8  27393  noseponlem  27632  recsne0  28188  tglnpt2  28713  midexlem  28764  colperpexlem3  28804  mideulem2  28806  lnopp2hpgb  28835  subgruhgredgd  29357  wwlksnext  29966  wspthsnonn0vne  29990  clwwisshclwws  30090  vdn0conngrumgrv2  30271  vdgn1frgrv2  30371  nrt2irr  30548  ifnetrue  32622  ifnefals  32623  imadifxp  32676  acunirnmpt  32737  fnpreimac  32749  quad3d  32829  xaddeq0  32833  pmtrcnelor  33173  domnprodn0  33357  domnprodeq0  33358  qsidomlem2  33534  ply1dg3rt0irred  33665  m1pmeq  33666  mplmulmvr  33704  esplyind  33731  ply1annnr  33860  minplyirred  33868  rtelextdg2lem  33883  constrrtcclem  33891  constrconj  33902  constrext2chnlem  33907  constrremulcl  33924  constrrecl  33926  constrreinvcl  33929  2sqr3minply  33937  2sqr3nconstr  33938  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  cos9thpiminply  33945  cos9thpinconstrlem1  33946  cos9thpinconstrlem2  33947  cos9thpinconstr  33948  madjusmdetlem2  33985  zar0ring  34035  xrge0iifhom  34094  signswn0  34717  signsvtn0  34727  signstfvneq0  34729  repr0  34768  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  wsuclem  36017  ivthALT  36529  neibastop1  36553  weiunfrlem  36658  finxpreclem2  37595  finxpreclem6  37601  tan2h  37813  poimirlem9  37830  heicant  37856  itg2addnclem2  37873  lsatfixedN  39269  islshpat  39277  lkrshp  39365  2llnm3N  39829  dalemdnee  39926  cdleme18b  40552  cdleme40m  40727  cdlemg12g  40909  cdlemh  41077  cdlemj3  41083  tendoconid  41089  cdlemk3  41093  cdlemk12  41110  cdlemk12u  41132  cdlemk46  41208  cdlemk54  41218  erngdvlem4  41251  erngdvlem4-rN  41259  dibn0  41413  dihglblem2aN  41553  dochshpncl  41644  dochsnnz  41710  dochsatshpb  41712  lcfl7lem  41759  lcfl8b  41764  lcfrlem33  41835  lcfr  41845  hdmaprnlem3uN  42111  aks4d1p1p7  42328  fldhmf1  42344  primrootspoweq0  42360  idomnnzpownz  42386  idomnnzgmulnz  42387  aks6d1c5lem2  42392  deg1gprod  42394  unitscyglem4  42452  tanhalfpim  42604  remul01  42662  remulinvcom  42688  domnexpgn0cl  42778  ricdrng1  42783  prjcrv0  42876  3cubeslem2  42927  cmpfiiin  42939  pell1234qrne0  43095  rmxyneg  43162  fnwe2lem2  43293  kelac1  43305  wnefimgd  44402  radcnvrat  44555  binomcxplemfrat  44592  binomcxplemradcnv  44593  disjrnmpt2  45432  disjf1o  45435  choicefi  45444  ioondisj2  45739  ioondisj1  45740  lptioo2  45877  lptioo1  45878  0ellimcdiv  45893  liminflbuz2  46059  ioodvbdlimc1  46177  ioodvbdlimc2  46179  stoweidlem31  46275  stoweidlem59  46303  wallispilem4  46312  wallispi  46314  stirlinglem3  46320  stirlinglem14  46331  dirkerper  46340  dirkertrigeq  46345  dirkercncflem2  46348  fourierdlem4  46355  fourierdlem30  46381  fourierdlem41  46392  fourierdlem42  46393  fourierdlem44  46395  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem62  46412  fourierdlem74  46424  fourierdlem75  46425  fourierdlem79  46429  fourierdlem102  46452  fourierdlem114  46464  fouriersw  46475  elaa2lem  46477  elaa2  46478  etransclem24  46502  etransclem44  46522  etransclem47  46525  ioorrnopnlem  46548  subsaliuncl  46602  sge0cl  46625  meadjun  46706  meadjiunlem  46709  hoicvr  46792  ovnsubadd2lem  46889  smflimlem6  47020  smfpimcc  47052  smflimsuplem2  47065  cjnpoly  47135  modm2nep1  47612  modm1nep2  47614  modm1p1ne  47616  lswn0  47690  sprvalpwn0  47729  fmtnoprmfac1lem  47810  grimuhgr  48133  gpg3nbgrvtx0  48322  el0ldep  48712  islindeps2  48729  ldepsnlinclem1  48751  ldepsnlinclem2  48752  itscnhlinecirc02plem1  49028  fvconstr  49107  fvconstrn0  49108  catprs  49256  fucofvalne  49570