Theorem eqnetrd 3009

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2941

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  eqnetrrd  3010  3netr4d  3019  opnz  5472  xpdifid  6164  undefne0  8259  onoviun  8338  intrnfi  9407  cantnfp1lem2  9670  cantnfp1lem3  9671  wemapwe  9688  acndom2  10045  fin23lem14  10324  fin23lem40  10342  isf32lem6  10349  isf34lem5  10369  isf34lem7  10370  isf34lem6  10371  axcc2lem  10427  xaddnemnf  13211  xaddnepnf  13212  fseqsupcl  13938  hashprg  14351  elprchashprn2  14352  hash1n0  14377  limsupgre  15421  isercolllem3  15609  prodfn0  15836  ntrivcvgtail  15842  fproddiv  15901  fprodn0  15919  tanval3  16073  tanneg  16087  ruclem11  16179  bezoutr1  16502  phibndlem  16699  dfphi2  16703  0ram  16949  0ram2  16950  ram0  16951  0ramcl  16952  gsumval2  18601  sgrp2nmndlem5  18806  issubg2  19015  ghmrn  19099  pmtrmvd  19317  gsumval3  19767  pgpfaclem2  19944  ablfaclem2  19948  ablfaclem3  19949  fincygsubgodd  19974  subdrgint  20407  abvdom  20434  lbsextlem2  20760  gzrngunit  20996  zringunit  21020  cnmsgnsubg  21114  frlmssuvc2  21334  mhpmulcl  21674  iinopn  22386  cnconn  22908  1stcfb  22931  dissnlocfin  23015  fbasrn  23370  fclscmpi  23515  alexsublem  23530  ustuqtop5  23732  cnextucn  23790  dscmet  24063  reperflem  24316  evth  24457  cmetcaulem  24787  iscmet3  24792  metsscmetcld  24814  cmetss  24815  bcthlem5  24827  bcth2  24829  mbflimsup  25165  itg1addlem4  25198  itg1addlem4OLD  25199  itg1climres  25214  itg2monolem1  25250  itg2i1fseq2  25256  tdeglem4  25559  tdeglem4OLD  25560  deg1add  25603  deg1mul2  25614  deg1tm  25618  dgreq  25740  dgradd2  25764  dgrmul  25766  dgrmulc  25767  dgrcolem1  25769  plyrem  25800  facth  25801  fta1lem  25802  vieta1lem1  25805  vieta1lem2  25806  vieta1  25807  qaa  25818  aareccl  25821  geolim3  25834  aaliou3lem9  25845  coseq00topi  25994  cosne0  26020  tanord  26029  tanarg  26109  cxpne0  26167  cxpsqrt  26193  logbrec  26267  chordthmlem  26317  chordthmlem2  26318  dcubic  26331  mcubic  26332  cubic2  26333  cubic  26334  quartlem4  26345  atandmneg  26391  atandmcj  26394  atancj  26395  atanrecl  26396  atanlogsublem  26400  efiatan2  26402  tanatan  26404  atandmtan  26405  cosatan  26406  cosatanne0  26407  wilthlem2  26553  ftalem7  26563  basellem2  26566  basellem4  26568  basellem5  26569  isppw  26598  dchrptlem2  26748  lgsne0  26818  2sqlem8a  26908  2sqlem8  26909  noseponlem  27147  tglnpt2  27872  midexlem  27923  colperpexlem3  27963  mideulem2  27965  lnopp2hpgb  27994  subgruhgredgd  28521  wwlksnext  29127  wspthsnonn0vne  29151  clwwisshclwws  29248  vdn0conngrumgrv2  29429  vdgn1frgrv2  29529  ifnetrue  31757  ifnefals  31758  imadifxp  31810  acunirnmpt  31862  fnpreimac  31874  xaddeq0  31944  pmtrcnelor  32230  qsidomlem2  32530  madjusmdetlem2  32746  zar0ring  32796  xrge0iifhom  32855  signswn0  33509  signsvtn0  33519  signstfvneq0  33521  repr0  33561  derangenlem  34100  subfacp1lem3  34111  subfacp1lem5  34113  wsuclem  34735  ivthALT  35158  neibastop1  35182  finxpreclem2  36209  finxpreclem6  36215  tan2h  36418  poimirlem9  36435  heicant  36461  itg2addnclem2  36478  lsatfixedN  37817  islshpat  37825  lkrshp  37913  2llnm3N  38378  dalemdnee  38475  cdleme18b  39101  cdleme40m  39276  cdlemg12g  39458  cdlemh  39626  cdlemj3  39632  tendoconid  39638  cdlemk3  39642  cdlemk12  39659  cdlemk12u  39681  cdlemk46  39757  cdlemk54  39767  erngdvlem4  39800  erngdvlem4-rN  39808  dibn0  39962  dihglblem2aN  40102  dochshpncl  40193  dochsnnz  40259  dochsatshpb  40261  lcfl7lem  40308  lcfl8b  40313  lcfrlem33  40384  lcfr  40394  hdmaprnlem3uN  40660  aks4d1p1p7  40877  fldhmf1  40893  metakunt7  40929  ricdrng1  41051  nn0rppwr  41167  remul01  41224  remulinvcom  41249  prjcrv0  41319  3cubeslem2  41356  cmpfiiin  41368  pell1234qrne0  41524  rmxyneg  41592  fnwe2lem2  41726  kelac1  41738  wnefimgd  42846  radcnvrat  43006  binomcxplemfrat  43043  binomcxplemradcnv  43044  disjrnmpt2  43819  disjf1o  43822  choicefi  43832  ioondisj2  44141  ioondisj1  44142  lptioo2  44282  lptioo1  44283  0ellimcdiv  44300  liminflbuz2  44466  ioodvbdlimc1  44584  ioodvbdlimc2  44586  stoweidlem31  44682  stoweidlem59  44710  wallispilem4  44719  wallispi  44721  stirlinglem3  44727  stirlinglem14  44738  dirkerper  44747  dirkertrigeq  44752  dirkercncflem2  44755  fourierdlem4  44762  fourierdlem30  44788  fourierdlem41  44799  fourierdlem42  44800  fourierdlem44  44802  fourierdlem46  44803  fourierdlem48  44805  fourierdlem49  44806  fourierdlem62  44819  fourierdlem74  44831  fourierdlem75  44832  fourierdlem79  44836  fourierdlem102  44859  fourierdlem114  44871  fouriersw  44882  elaa2lem  44884  elaa2  44885  etransclem24  44909  etransclem44  44929  etransclem47  44932  ioorrnopnlem  44955  subsaliuncl  45009  sge0cl  45032  meadjun  45113  meadjiunlem  45116  hoicvr  45199  ovnsubadd2lem  45296  smflimlem6  45427  smfpimcc  45459  smflimsuplem2  45472  lswn0  46047  sprvalpwn0  46086  fmtnoprmfac1lem  46167  el0ldep  47049  islindeps2  47066  ldepsnlinclem1  47088  ldepsnlinclem2  47089  itscnhlinecirc02plem1  47370  fvconstr  47424  fvconstrn0  47425  catprs  47533