Theorem eqnetrd 3012

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ne 2945

This theorem is referenced by:  eqnetrrd  3013  3netr4d  3022  opnz  5389  xpdifid  6076  undefne0  8104  onoviun  8183  intrnfi  9184  cantnfp1lem2  9446  cantnfp1lem3  9447  wemapwe  9464  acndom2  9819  fin23lem14  10098  fin23lem40  10116  isf32lem6  10123  isf34lem5  10143  isf34lem7  10144  isf34lem6  10145  axcc2lem  10201  xaddnemnf  12979  xaddnepnf  12980  fseqsupcl  13706  hashprg  14119  elprchashprn2  14120  hash1n0  14145  limsupgre  15199  isercolllem3  15387  prodfn0  15615  ntrivcvgtail  15621  fproddiv  15680  fprodn0  15698  tanval3  15852  tanneg  15866  ruclem11  15958  bezoutr1  16283  phibndlem  16480  dfphi2  16484  0ram  16730  0ram2  16731  ram0  16732  0ramcl  16733  gsumval2  18379  sgrp2nmndlem5  18577  issubg2  18779  ghmrn  18856  pmtrmvd  19073  gsumval3  19517  pgpfaclem2  19694  ablfaclem2  19698  ablfaclem3  19699  fincygsubgodd  19724  subdrgint  20080  abvdom  20107  lbsextlem2  20430  gzrngunit  20673  zringunit  20697  cnmsgnsubg  20791  frlmssuvc2  21011  mhpmulcl  21348  iinopn  22060  cnconn  22582  1stcfb  22605  dissnlocfin  22689  fbasrn  23044  fclscmpi  23189  alexsublem  23204  ustuqtop5  23406  cnextucn  23464  dscmet  23737  reperflem  23990  evth  24131  cmetcaulem  24461  iscmet3  24466  metsscmetcld  24488  cmetss  24489  bcthlem5  24501  bcth2  24503  mbflimsup  24839  itg1addlem4  24872  itg1addlem4OLD  24873  itg1climres  24888  itg2monolem1  24924  itg2i1fseq2  24930  tdeglem4  25233  tdeglem4OLD  25234  deg1add  25277  deg1mul2  25288  deg1tm  25292  dgreq  25414  dgradd2  25438  dgrmul  25440  dgrmulc  25441  dgrcolem1  25443  plyrem  25474  facth  25475  fta1lem  25476  vieta1lem1  25479  vieta1lem2  25480  vieta1  25481  qaa  25492  aareccl  25495  geolim3  25508  aaliou3lem9  25519  coseq00topi  25668  cosne0  25694  tanord  25703  tanarg  25783  cxpne0  25841  cxpsqrt  25867  logbrec  25941  chordthmlem  25991  chordthmlem2  25992  dcubic  26005  mcubic  26006  cubic2  26007  cubic  26008  quartlem4  26019  atandmneg  26065  atandmcj  26068  atancj  26069  atanrecl  26070  atanlogsublem  26074  efiatan2  26076  tanatan  26078  atandmtan  26079  cosatan  26080  cosatanne0  26081  wilthlem2  26227  ftalem7  26237  basellem2  26240  basellem4  26242  basellem5  26243  isppw  26272  dchrptlem2  26422  lgsne0  26492  2sqlem8a  26582  2sqlem8  26583  tglnpt2  27011  midexlem  27062  colperpexlem3  27102  mideulem2  27104  lnopp2hpgb  27133  subgruhgredgd  27660  wwlksnext  28267  wspthsnonn0vne  28291  clwwisshclwws  28388  vdn0conngrumgrv2  28569  vdgn1frgrv2  28669  imadifxp  30949  acunirnmpt  31005  fnpreimac  31017  xaddeq0  31085  pmtrcnelor  31369  qsidomlem2  31638  madjusmdetlem2  31787  zar0ring  31837  xrge0iifhom  31896  signswn0  32548  signsvtn0  32558  signstfvneq0  32560  repr0  32600  derangenlem  33142  subfacp1lem3  33153  subfacp1lem5  33155  wsuclem  33828  noseponlem  33876  ivthALT  34533  neibastop1  34557  finxpreclem2  35570  finxpreclem6  35576  tan2h  35778  poimirlem9  35795  heicant  35821  itg2addnclem2  35838  lsatfixedN  37030  islshpat  37038  lkrshp  37126  2llnm3N  37590  dalemdnee  37687  cdleme18b  38313  cdleme40m  38488  cdlemg12g  38670  cdlemh  38838  cdlemj3  38844  tendoconid  38850  cdlemk3  38854  cdlemk12  38871  cdlemk12u  38893  cdlemk46  38969  cdlemk54  38979  erngdvlem4  39012  erngdvlem4-rN  39020  dibn0  39174  dihglblem2aN  39314  dochshpncl  39405  dochsnnz  39471  dochsatshpb  39473  lcfl7lem  39520  lcfl8b  39525  lcfrlem33  39596  lcfr  39606  hdmaprnlem3uN  39872  aks4d1p1p7  40089  metakunt7  40138  nn0rppwr  40340  remul01  40397  remulinvcom  40421  3cubeslem2  40514  cmpfiiin  40526  pell1234qrne0  40682  rmxyneg  40749  fnwe2lem2  40883  kelac1  40895  wnefimgd  41779  radcnvrat  41939  binomcxplemfrat  41976  binomcxplemradcnv  41977  disjrnmpt2  42733  disjf1o  42736  choicefi  42747  ioondisj2  43038  ioondisj1  43039  lptioo2  43179  lptioo1  43180  0ellimcdiv  43197  liminflbuz2  43363  ioodvbdlimc1  43481  ioodvbdlimc2  43483  stoweidlem31  43579  stoweidlem59  43607  wallispilem4  43616  wallispi  43618  stirlinglem3  43624  stirlinglem14  43635  dirkerper  43644  dirkertrigeq  43649  dirkercncflem2  43652  fourierdlem4  43659  fourierdlem30  43685  fourierdlem41  43696  fourierdlem42  43697  fourierdlem44  43699  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem62  43716  fourierdlem74  43728  fourierdlem75  43729  fourierdlem79  43733  fourierdlem102  43756  fourierdlem114  43768  fouriersw  43779  elaa2lem  43781  elaa2  43782  etransclem24  43806  etransclem44  43826  etransclem47  43829  ioorrnopnlem  43852  subsaliuncl  43904  sge0cl  43926  meadjun  44007  meadjiunlem  44010  hoicvr  44093  ovnsubadd2lem  44190  smflimlem6  44321  smfpimcc  44352  smflimsuplem2  44365  lswn0  44907  sprvalpwn0  44946  fmtnoprmfac1lem  45027  el0ldep  45818  islindeps2  45835  ldepsnlinclem1  45857  ldepsnlinclem2  45858  itscnhlinecirc02plem1  46139  fvconstr  46194  fvconstrn0  46195  catprs  46303