Theorem eqnetrd 2861

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

Syntax hints:   → wi 4   = wceq 1483   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  eqnetrrd  2862  3netr4d  2871  opnz  4942  xpdifid  5562  undefne0  7405  onoviun  7440  intrnfi  8322  cantnfp1lem2  8576  cantnfp1lem3  8577  wemapwe  8594  acndom2  8877  fin23lem14  9155  fin23lem40  9173  isf32lem6  9180  isf34lem5  9200  isf34lem7  9201  isf34lem6  9202  axcc2lem  9258  xaddnemnf  12067  xaddnepnf  12068  fseqsupcl  12776  hashprg  13182  hashprgOLD  13183  elprchashprn2  13184  hash1n0  13209  limsupgre  14212  isercolllem3  14397  prodfn0  14626  ntrivcvgtail  14632  fproddiv  14691  fprodn0  14709  tanval3  14864  tanneg  14878  ruclem11  14969  bezoutr1  15282  phibndlem  15475  dfphi2  15479  0ram  15724  0ram2  15725  ram0  15726  0ramcl  15727  gsumval2  17280  sgrp2nmndlem5  17416  issubg2  17609  ghmrn  17673  pmtrmvd  17876  gsumval3  18308  pgpfaclem2  18481  ablfaclem2  18485  ablfaclem3  18486  abvdom  18838  lbsextlem2  19159  gzrngunit  19812  zringunit  19836  cnmsgnsubg  19923  frlmssuvc2  20134  iinopn  20707  cnconn  21225  1stcfb  21248  dissnlocfin  21332  fbasrn  21688  fclscmpi  21833  alexsublem  21848  ustuqtop5  22049  cnextucn  22107  dscmet  22377  reperflem  22621  evth  22758  cmetcaulem  23086  iscmet3  23091  cmetss  23113  bcthlem5  23125  bcth2  23127  mbflimsup  23433  itg1addlem4  23466  itg1climres  23481  itg2monolem1  23517  itg2i1fseq2  23523  tdeglem4  23820  deg1add  23863  deg1mul2  23874  deg1tm  23878  dgreq  24000  dgradd2  24024  dgrmul  24026  dgrmulc  24027  dgrcolem1  24029  plyrem  24060  facth  24061  fta1lem  24062  vieta1lem1  24065  vieta1lem2  24066  vieta1  24067  qaa  24078  aareccl  24081  geolim3  24094  aaliou3lem9  24105  coseq00topi  24254  cosne0  24276  tanord  24284  tanarg  24365  cxpne0  24423  cxpsqrt  24449  logbrec  24520  chordthmlem  24559  chordthmlem2  24560  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  quartlem4  24587  atandmneg  24633  atandmcj  24636  atancj  24637  atanrecl  24638  atanlogsublem  24642  efiatan2  24644  tanatan  24646  atandmtan  24647  cosatan  24648  cosatanne0  24649  wilthlem2  24795  ftalem7  24805  basellem2  24808  basellem4  24810  basellem5  24811  isppw  24840  dchrptlem2  24990  lgsne0  25060  2sqlem8a  25150  2sqlem8  25151  tglnpt2  25536  midexlem  25587  colperpexlem3  25624  mideulem2  25626  lnopp2hpgb  25655  subgruhgredgd  26176  wwlksnext  26788  wspthsnonn0vne  26813  clwwisshclwws  26928  vdn0conngrumgrv2  27056  vdgn1frgrv2  27160  imadifxp  29414  acunirnmpt  29459  nn0sqeq1  29513  xaddeq0  29518  madjusmdetlem2  29894  xrge0iifhom  29983  signswn0  30637  signsvtn0  30647  signstfvneq0  30649  repr0  30689  derangenlem  31153  subfacp1lem3  31164  subfacp1lem5  31166  wsuclem  31773  wsuclemOLD  31774  noseponlem  31817  ivthALT  32330  neibastop1  32354  finxpreclem2  33227  finxpreclem6  33233  tan2h  33401  poimirlem9  33418  heicant  33444  itg2addnclem2  33462  lsatfixedN  34296  islshpat  34304  lkrshp  34392  2llnm3N  34855  dalemdnee  34952  cdleme18b  35579  cdleme40m  35755  cdlemg12g  35937  cdlemh  36105  cdlemj3  36111  tendoconid  36117  cdlemk3  36121  cdlemk12  36138  cdlemk12u  36160  cdlemk46  36236  cdlemk54  36246  erngdvlem4  36279  erngdvlem4-rN  36287  dibn0  36442  dihglblem2aN  36582  dochshpncl  36673  dochsnnz  36739  dochsatshpb  36741  lcfl7lem  36788  lcfl8b  36793  lcfrlem33  36864  lcfr  36874  hdmaprnlem3uN  37143  cmpfiiin  37260  pell1234qrne0  37417  rmxyneg  37485  fnwe2lem2  37621  kelac1  37633  wnefimgd  38460  radcnvrat  38513  binomcxplemfrat  38550  binomcxplemradcnv  38551  disjrnmpt2  39375  disjf1o  39378  choicefi  39392  ioondisj2  39714  ioondisj1  39715  lptioo2  39863  lptioo1  39864  0ellimcdiv  39881  ioodvbdlimc1  40148  ioodvbdlimc2  40150  stoweidlem31  40248  stoweidlem59  40276  wallispilem4  40285  wallispi  40287  stirlinglem3  40293  stirlinglem14  40304  dirkerper  40313  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem4  40328  fourierdlem30  40354  fourierdlem41  40365  fourierdlem42  40366  fourierdlem44  40368  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem62  40385  fourierdlem74  40397  fourierdlem75  40398  fourierdlem79  40402  fourierdlem102  40425  fourierdlem114  40437  fouriersw  40448  elaa2lem  40450  elaa2  40451  etransclem24  40475  etransclem44  40495  etransclem47  40498  ioorrnopnlem  40524  subsaliuncl  40576  sge0cl  40598  meadjun  40679  meadjiunlem  40682  hoicvr  40762  ovnsubadd2lem  40859  smflimlem6  40984  smfpimcc  41014  smflimsuplem2  41027  lswn0  41380  pfxn0  41394  fmtnoprmfac1lem  41476  sprvalpwn0  41733  el0ldep  42255  islindeps2  42272  ldepsnlinclem1  42294  ldepsnlinclem2  42295