Theorem eqnetrd 2998

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ne 2932

This theorem is referenced by:  eqnetrrd  2999  3netr4d  3008  opnz  5458  xpdifid  6168  undefne0  8286  onoviun  8365  intrnfi  9438  cantnfp1lem2  9701  cantnfp1lem3  9702  wemapwe  9719  acndom2  10076  fin23lem14  10355  fin23lem40  10373  isf32lem6  10380  isf34lem5  10400  isf34lem7  10401  isf34lem6  10402  axcc2lem  10458  xaddnemnf  13260  xaddnepnf  13261  fseqsupcl  14000  hashprg  14416  elprchashprn2  14417  hash1n0  14442  limsupgre  15499  isercolllem3  15685  prodfn0  15912  ntrivcvgtail  15918  fproddiv  15979  fprodn0  15997  tanval3  16152  tanneg  16166  ruclem11  16258  nn0rppwr  16580  bezoutr1  16588  phibndlem  16789  dfphi2  16793  0ram  17040  0ram2  17041  ram0  17042  0ramcl  17043  gsumval2  18668  sgrp2nmndlem5  18911  issubg2  19128  ghmrn  19216  pmtrmvd  19442  gsumval3  19893  pgpfaclem2  20070  ablfaclem2  20074  ablfaclem3  20075  fincygsubgodd  20100  subdrgint  20772  abvdom  20799  lbsextlem2  21129  cndrng  21373  gzrngunit  21413  zringunit  21439  cnmsgnsubg  21549  frlmssuvc2  21769  mhpmulcl  22101  iinopn  22856  cnconn  23376  1stcfb  23399  dissnlocfin  23483  fbasrn  23838  fclscmpi  23983  alexsublem  23998  ustuqtop5  24200  cnextucn  24257  dscmet  24529  reperflem  24776  evth  24927  cmetcaulem  25258  iscmet3  25263  metsscmetcld  25285  cmetss  25286  bcthlem5  25298  bcth2  25300  mbflimsup  25637  itg1addlem4  25670  itg1climres  25685  itg2monolem1  25721  itg2i1fseq2  25727  tdeglem4  26035  deg1add  26078  deg1mul2  26089  deg1tm  26094  dgreq  26219  dgradd2  26244  dgrmul  26246  dgrmulc  26247  dgrcolem1  26249  plyrem  26283  facth  26284  fta1lem  26285  vieta1lem1  26288  vieta1lem2  26289  vieta1  26290  qaa  26301  aareccl  26304  geolim3  26317  aaliou3lem9  26328  coseq00topi  26480  cosne0  26507  tanord  26516  tanarg  26597  cxpne0  26655  cxpsqrt  26681  logbrec  26761  chordthmlem  26811  chordthmlem2  26812  dcubic  26825  mcubic  26826  cubic2  26827  cubic  26828  quartlem4  26839  atandmneg  26885  atandmcj  26888  atancj  26889  atanrecl  26890  atanlogsublem  26894  efiatan2  26896  tanatan  26898  atandmtan  26899  cosatan  26900  cosatanne0  26901  wilthlem2  27048  ftalem7  27058  basellem2  27061  basellem4  27063  basellem5  27064  isppw  27093  dchrptlem2  27245  lgsne0  27315  2sqlem8a  27405  2sqlem8  27406  noseponlem  27645  tglnpt2  28585  midexlem  28636  colperpexlem3  28676  mideulem2  28678  lnopp2hpgb  28707  subgruhgredgd  29229  wwlksnext  29841  wspthsnonn0vne  29865  clwwisshclwws  29962  vdn0conngrumgrv2  30143  vdgn1frgrv2  30243  nrt2irr  30420  ifnetrue  32495  ifnefals  32496  imadifxp  32549  acunirnmpt  32604  fnpreimac  32616  quad3d  32690  xaddeq0  32693  pmtrcnelor  33050  domnprodn0  33218  qsidomlem2  33416  ply1dg3rt0irred  33542  m1pmeq  33543  ply1annnr  33683  minplyirred  33691  rtelextdg2lem  33706  constrrtcclem  33714  constrconj  33725  constrext2chnlem  33730  constrremulcl  33747  2sqr3minply  33749  2sqr3nconstr  33750  madjusmdetlem2  33786  zar0ring  33836  xrge0iifhom  33895  signswn0  34534  signsvtn0  34544  signstfvneq0  34546  repr0  34585  derangenlem  35135  subfacp1lem3  35146  subfacp1lem5  35148  wsuclem  35785  ivthALT  36295  neibastop1  36319  weiunfrlem  36424  finxpreclem2  37350  finxpreclem6  37356  tan2h  37578  poimirlem9  37595  heicant  37621  itg2addnclem2  37638  lsatfixedN  38969  islshpat  38977  lkrshp  39065  2llnm3N  39530  dalemdnee  39627  cdleme18b  40253  cdleme40m  40428  cdlemg12g  40610  cdlemh  40778  cdlemj3  40784  tendoconid  40790  cdlemk3  40794  cdlemk12  40811  cdlemk12u  40833  cdlemk46  40909  cdlemk54  40919  erngdvlem4  40952  erngdvlem4-rN  40960  dibn0  41114  dihglblem2aN  41254  dochshpncl  41345  dochsnnz  41411  dochsatshpb  41413  lcfl7lem  41460  lcfl8b  41465  lcfrlem33  41536  lcfr  41546  hdmaprnlem3uN  41812  aks4d1p1p7  42034  fldhmf1  42050  primrootspoweq0  42066  idomnnzpownz  42092  idomnnzgmulnz  42093  aks6d1c5lem2  42098  deg1gprod  42100  unitscyglem4  42158  metakunt7  42171  tanhalfpim  42348  remul01  42400  remulinvcom  42425  domnexpgn0cl  42496  ricdrng1  42501  prjcrv0  42606  3cubeslem2  42659  cmpfiiin  42671  pell1234qrne0  42827  rmxyneg  42895  fnwe2lem2  43026  kelac1  43038  wnefimgd  44136  radcnvrat  44290  binomcxplemfrat  44327  binomcxplemradcnv  44328  disjrnmpt2  45150  disjf1o  45153  choicefi  45162  ioondisj2  45463  ioondisj1  45464  lptioo2  45603  lptioo1  45604  0ellimcdiv  45621  liminflbuz2  45787  ioodvbdlimc1  45905  ioodvbdlimc2  45907  stoweidlem31  46003  stoweidlem59  46031  wallispilem4  46040  wallispi  46042  stirlinglem3  46048  stirlinglem14  46059  dirkerper  46068  dirkertrigeq  46073  dirkercncflem2  46076  fourierdlem4  46083  fourierdlem30  46109  fourierdlem41  46120  fourierdlem42  46121  fourierdlem44  46123  fourierdlem46  46124  fourierdlem48  46126  fourierdlem49  46127  fourierdlem62  46140  fourierdlem74  46152  fourierdlem75  46153  fourierdlem79  46157  fourierdlem102  46180  fourierdlem114  46192  fouriersw  46203  elaa2lem  46205  elaa2  46206  etransclem24  46230  etransclem44  46250  etransclem47  46253  ioorrnopnlem  46276  subsaliuncl  46330  sge0cl  46353  meadjun  46434  meadjiunlem  46437  hoicvr  46520  ovnsubadd2lem  46617  smflimlem6  46748  smfpimcc  46780  smflimsuplem2  46793  lswn0  47389  sprvalpwn0  47428  fmtnoprmfac1lem  47509  grimuhgr  47836  gpg3nbgrvtx0  47990  el0ldep  48341  islindeps2  48358  ldepsnlinclem1  48380  ldepsnlinclem2  48381  itscnhlinecirc02plem1  48661  fvconstr  48723  fvconstrn0  48724  catprs  48868  fucofvalne  48996