Theorem eqnetrd 3086

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

Syntax hints:   → wi 4   = wceq 1536   ≠ wne 3019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-ne 3020

This theorem is referenced by:  eqnetrrd  3087  3netr4d  3096  opnz  5368  xpdifid  6028  undefne0  7948  onoviun  7983  intrnfi  8883  cantnfp1lem2  9145  cantnfp1lem3  9146  wemapwe  9163  acndom2  9483  fin23lem14  9758  fin23lem40  9776  isf32lem6  9783  isf34lem5  9803  isf34lem7  9804  isf34lem6  9805  axcc2lem  9861  xaddnemnf  12632  xaddnepnf  12633  fseqsupcl  13348  hashprg  13759  elprchashprn2  13760  hash1n0  13785  limsupgre  14841  isercolllem3  15026  prodfn0  15253  ntrivcvgtail  15259  fproddiv  15318  fprodn0  15336  tanval3  15490  tanneg  15504  ruclem11  15596  bezoutr1  15916  phibndlem  16110  dfphi2  16114  0ram  16359  0ram2  16360  ram0  16361  0ramcl  16362  gsumval2  17899  sgrp2nmndlem5  18097  issubg2  18297  ghmrn  18374  pmtrmvd  18587  gsumval3  19030  pgpfaclem2  19207  ablfaclem2  19211  ablfaclem3  19212  fincygsubgodd  19237  subdrgint  19585  abvdom  19612  lbsextlem2  19934  gzrngunit  20614  zringunit  20638  cnmsgnsubg  20724  frlmssuvc2  20942  iinopn  21513  cnconn  22033  1stcfb  22056  dissnlocfin  22140  fbasrn  22495  fclscmpi  22640  alexsublem  22655  ustuqtop5  22857  cnextucn  22915  dscmet  23185  reperflem  23429  evth  23566  cmetcaulem  23894  iscmet3  23899  metsscmetcld  23921  cmetss  23922  bcthlem5  23934  bcth2  23936  mbflimsup  24270  itg1addlem4  24303  itg1climres  24318  itg2monolem1  24354  itg2i1fseq2  24360  tdeglem4  24657  deg1add  24700  deg1mul2  24711  deg1tm  24715  dgreq  24837  dgradd2  24861  dgrmul  24863  dgrmulc  24864  dgrcolem1  24866  plyrem  24897  facth  24898  fta1lem  24899  vieta1lem1  24902  vieta1lem2  24903  vieta1  24904  qaa  24915  aareccl  24918  geolim3  24931  aaliou3lem9  24942  coseq00topi  25091  cosne0  25117  tanord  25125  tanarg  25205  cxpne0  25263  cxpsqrt  25289  logbrec  25363  chordthmlem  25413  chordthmlem2  25414  dcubic  25427  mcubic  25428  cubic2  25429  cubic  25430  quartlem4  25441  atandmneg  25487  atandmcj  25490  atancj  25491  atanrecl  25492  atanlogsublem  25496  efiatan2  25498  tanatan  25500  atandmtan  25501  cosatan  25502  cosatanne0  25503  wilthlem2  25649  ftalem7  25659  basellem2  25662  basellem4  25664  basellem5  25665  isppw  25694  dchrptlem2  25844  lgsne0  25914  2sqlem8a  26004  2sqlem8  26005  tglnpt2  26430  midexlem  26481  colperpexlem3  26521  mideulem2  26523  lnopp2hpgb  26552  subgruhgredgd  27069  wwlksnext  27674  wspthsnonn0vne  27699  clwwisshclwws  27796  vdn0conngrumgrv2  27978  vdgn1frgrv2  28078  imadifxp  30354  acunirnmpt  30407  fnpreimac  30419  xaddeq0  30480  pmtrcnelor  30739  qsidomlem2  30970  madjusmdetlem2  31097  xrge0iifhom  31184  signswn0  31834  signsvtn0  31844  signstfvneq0  31846  repr0  31886  derangenlem  32422  subfacp1lem3  32433  subfacp1lem5  32435  wsuclem  33116  noseponlem  33175  ivthALT  33687  neibastop1  33711  finxpreclem2  34675  finxpreclem6  34681  tan2h  34888  poimirlem9  34905  heicant  34931  itg2addnclem2  34948  lsatfixedN  36149  islshpat  36157  lkrshp  36245  2llnm3N  36709  dalemdnee  36806  cdleme18b  37432  cdleme40m  37607  cdlemg12g  37789  cdlemh  37957  cdlemj3  37963  tendoconid  37969  cdlemk3  37973  cdlemk12  37990  cdlemk12u  38012  cdlemk46  38088  cdlemk54  38098  erngdvlem4  38131  erngdvlem4-rN  38139  dibn0  38293  dihglblem2aN  38433  dochshpncl  38524  dochsnnz  38590  dochsatshpb  38592  lcfl7lem  38639  lcfl8b  38644  lcfrlem33  38715  lcfr  38725  hdmaprnlem3uN  38991  nn0rppwr  39188  remul01  39243  remulinvcom  39254  3cubeslem2  39288  cmpfiiin  39300  pell1234qrne0  39456  rmxyneg  39523  fnwe2lem2  39657  kelac1  39669  wnefimgd  40518  radcnvrat  40652  binomcxplemfrat  40689  binomcxplemradcnv  40690  disjrnmpt2  41455  disjf1o  41458  choicefi  41469  ioondisj2  41773  ioondisj1  41774  lptioo2  41918  lptioo1  41919  0ellimcdiv  41936  liminflbuz2  42102  ioodvbdlimc1  42224  ioodvbdlimc2  42226  stoweidlem31  42323  stoweidlem59  42351  wallispilem4  42360  wallispi  42362  stirlinglem3  42368  stirlinglem14  42379  dirkerper  42388  dirkertrigeq  42393  dirkercncflem2  42396  fourierdlem4  42403  fourierdlem30  42429  fourierdlem41  42440  fourierdlem42  42441  fourierdlem44  42443  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem62  42460  fourierdlem74  42472  fourierdlem75  42473  fourierdlem79  42477  fourierdlem102  42500  fourierdlem114  42512  fouriersw  42523  elaa2lem  42525  elaa2  42526  etransclem24  42550  etransclem44  42570  etransclem47  42573  ioorrnopnlem  42596  subsaliuncl  42648  sge0cl  42670  meadjun  42751  meadjiunlem  42754  hoicvr  42837  ovnsubadd2lem  42934  smflimlem6  43059  smfpimcc  43089  smflimsuplem2  43102  lswn0  43611  sprvalpwn0  43652  fmtnoprmfac1lem  43733  el0ldep  44528  islindeps2  44545  ldepsnlinclem1  44567  ldepsnlinclem2  44568  itscnhlinecirc02plem1  44776