Theorem eqnetrd 3027

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ne 2961

This theorem is used by:  eqnetrrd  3028  3netr4d  3037  opnz  5457  xpdifid  6167  undefne0  8278  onoviun  8332  intrnfi  9379  cantnfp1lem2  9651  cantnfp1lem3  9652  wemapwe  9669  acndom2  10050  fin23lem14  10328  fin23lem40  10346  isf32lem6  10353  isf34lem5  10373  isf34lem7  10374  isf34lem6  10375  axcc2lem  10431  xaddnemnf  13273  xaddnepnf  13274  fseqsupcl  14026  hashprg  14444  elprchashprn2  14445  hash1n0  14471  limsupgre  15551  isercolllem3  15737  prodfn0  15966  ntrivcvgtail  15972  fproddiv  16033  fprodn0  16051  tanval3  16207  tanneg  16221  ruclem11  16313  nn0rppwr  16636  bezoutr1  16644  phibndlem  16846  dfphi2  16850  0ram  17097  0ram2  17098  ram0  17099  0ramcl  17100  gsumval2  18765  sgrp2nmndlem5  19014  issubg2  19231  ghmrn  19322  pmtrmvd  19549  gsumval3  20000  pgpfaclem2  20177  ablfaclem2  20181  ablfaclem3  20182  fincygsubgodd  20207  subdrgint  20935  abvdom  20962  lbsextlem2  21312  qsidomlem2  21510  cndrng  21580  gzrngunit  21612  zringunit  21645  cnmsgnsubg  21756  frlmssuvc2  21974  mhpmulcl  22341  iinopn  23088  cnconn  23608  1stcfb  23631  dissnlocfin  23715  fbasrn  24070  fclscmpi  24215  alexsublem  24230  ustuqtop5  24431  cnextucn  24488  dscmet  24758  reperflem  25005  evth  25147  cmetcaulem  25476  iscmet3  25481  metsscmetcld  25503  cmetss  25504  bcthlem5  25516  bcth2  25518  mbflimsup  25854  itg1addlem4  25887  itg1climres  25902  itg2monolem1  25938  itg2i1fseq2  25944  tdeglem4  26246  deg1add  26289  deg1mul2  26300  deg1tm  26305  dgreq  26430  dgradd2  26454  dgrmul  26456  dgrmulc  26457  dgrcolem1  26459  plyrem  26495  facth  26496  fta1lem  26497  vieta1lem1  26500  vieta1lem2  26501  vieta1  26502  qaa  26513  aareccl  26518  geolim3  26531  aaliou3lem9  26542  coseq00topi  26696  cosne0  26723  tanord  26732  tanarg  26813  cxpne0  26871  cxpsqrt  26897  logbrec  26976  chordthmlem  27026  chordthmlem2  27027  dcubic  27040  mcubic  27041  cubic2  27042  cubic  27043  quartlem4  27054  atandmneg  27100  atandmcj  27103  atancj  27104  atanrecl  27105  atanlogsublem  27109  efiatan2  27111  tanatan  27113  atandmtan  27114  cosatan  27115  cosatanne0  27116  wilthlem2  27262  ftalem7  27272  basellem2  27275  basellem4  27277  basellem5  27278  isppw  27307  dchrptlem2  27458  lgsne0  27528  2sqlem8a  27618  2sqlem8  27619  noseponlem  27857  recsne0  28414  tglnpt2  28955  midexlem  28998  colperpexlem3  29042  mideulem2  29044  lnopp2hpgb  29074  subgruhgredgd  29663  wwlksnext  30271  wspthsnonn0vne  30295  clwwisshclwws  30395  vdn0conngrumgrv2  30576  vdgn1frgrv2  30676  nrt2irr  30853  ifnetrue  32922  ifnefals  32923  imadifxp  32975  acunirnmpt  33033  fnpreimac  33044  quad3d  33123  xaddeq0  33127  pmtrcnelor  33434  domnprodn0  33621  domnprodeq0  33622  drnglring  33805  dflringlem3  33809  dflring4  33811  ply1dg3rt0irred  33897  m1pmeq  33898  mplmulmvr  33952  esplyfvaln  33987  esplyind  33988  ply1annnr  34116  minplyirred  34124  rtelextdg2lem  34139  constrrtcclem  34147  constrconj  34158  constrext2chnlem  34163  constrremulcl  34180  constrrecl  34182  constrreinvcl  34185  2sqr3minply  34193  2sqr3nconstr  34194  cos9thpiminplylem1  34195  cos9thpiminplylem2  34196  cos9thpiminplylem3  34197  cos9thpiminply  34201  cos9thpinconstrlem1  34202  cos9thpinconstrlem2  34203  cos9thpinconstr  34204  madjusmdetlem2  34241  zar0ring  34291  xrge0iifhom  34350  signswn0  34971  signsvtn0  34981  signstfvneq0  34983  repr0  35022  kard0b  35588  derangenlem  35676  subfacp1lem3  35687  subfacp1lem5  35689  wsuclem  36328  ivthALT  36879  neibastop1  36903  weiunfrlem  37008  finxpreclem2  38069  finxpreclem6  38075  tan2h  38296  poimirlem9  38313  heicant  38339  itg2addnclem2  38356  lsatfixedN  39816  islshpat  39824  lkrshp  39912  2llnm3N  40376  dalemdnee  40473  cdleme18b  41099  cdleme40m  41274  cdlemg12g  41456  cdlemh  41624  cdlemj3  41630  tendoconid  41636  cdlemk3  41640  cdlemk12  41657  cdlemk12u  41679  cdlemk46  41755  cdlemk54  41765  erngdvlem4  41798  erngdvlem4-rN  41806  dibn0  41960  dihglblem2aN  42100  dochshpncl  42191  dochsnnz  42257  dochsatshpb  42259  lcfl7lem  42306  lcfl8b  42311  lcfrlem33  42382  lcfr  42392  hdmaprnlem3uN  42658  aks4d1p1p7  42874  fldhmf1  42890  primrootspoweq0  42906  idomnnzpownz  42932  idomnnzgmulnz  42933  aks6d1c5lem2  42938  deg1gprod  42940  unitscyglem4  42998  25or6to4  43006  tanhalfpim  43143  remul01  43201  remulinvcom  43227  domnexpgn0cl  43324  ricdrng1  43329  prjcrv0  43398  3cubeslem2  43449  cmpfiiin  43461  pell1234qrne0  43613  rmxyneg  43680  fnwe2lem2  43811  kelac1  43823  wnefimgd  44920  radcnvrat  45057  binomcxplemfrat  45094  binomcxplemradcnv  45095  disjrnmpt2  45939  disjf1o  45942  choicefi  45950  ioondisj2  46242  ioondisj1  46243  lptioo2  46380  lptioo1  46381  0ellimcdiv  46396  liminflbuz2  46562  ioodvbdlimc1  46680  ioodvbdlimc2  46682  stoweidlem31  46778  stoweidlem59  46806  wallispilem4  46815  wallispi  46817  stirlinglem3  46823  stirlinglem14  46834  dirkerper  46843  dirkertrigeq  46848  dirkercncflem2  46851  fourierdlem4  46858  fourierdlem30  46884  fourierdlem41  46895  fourierdlem42  46896  fourierdlem44  46898  fourierdlem46  46899  fourierdlem48  46901  fourierdlem49  46902  fourierdlem62  46915  fourierdlem74  46927  fourierdlem75  46928  fourierdlem79  46932  fourierdlem102  46955  fourierdlem114  46967  fouriersw  46978  elaa2lem  46980  elaa2  46981  etransclem24  47005  etransclem44  47025  etransclem47  47028  ioorrnopnlem  47051  subsaliuncl  47105  sge0cl  47128  meadjun  47209  meadjiunlem  47212  hoicvr  47295  ovnsubadd2lem  47392  smflimlem6  47523  smfpimcc  47555  smflimsuplem2  47568  sqrtnnaa  47637  sqrtnzqaa  47638  cjnpoly  47659  modm2nep1  48142  modm1nep2  48144  modm1p1ne  48146  lswn0  48226  sprvalpwn0  48265  fmtnoprmfac1lem  48349  grimuhgr  48685  gpg3nbgrvtx0  48874  el0ldep  49279  islindeps2  49296  ldepsnlinclem1  49318  ldepsnlinclem2  49319  itscnhlinecirc02plem1  49595  fvconstr  49673  fvconstrn0  49674  catprs  49822  fucofvalne  50136  crosspv2i  50676  crosspv3i  50677