Theorem eqnetrd 2995

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

Syntax hints:   → wi 4   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  eqnetrrd  2996  3netr4d  3005  opnz  5408  xpdifid  6110  undefne0  8204  onoviun  8258  intrnfi  9295  cantnfp1lem2  9564  cantnfp1lem3  9565  wemapwe  9582  acndom2  9940  fin23lem14  10219  fin23lem40  10237  isf32lem6  10244  isf34lem5  10264  isf34lem7  10265  isf34lem6  10266  axcc2lem  10322  xaddnemnf  13130  xaddnepnf  13131  fseqsupcl  13879  hashprg  14297  elprchashprn2  14298  hash1n0  14323  limsupgre  15383  isercolllem3  15569  prodfn0  15796  ntrivcvgtail  15802  fproddiv  15863  fprodn0  15881  tanval3  16038  tanneg  16052  ruclem11  16144  nn0rppwr  16467  bezoutr1  16475  phibndlem  16676  dfphi2  16680  0ram  16927  0ram2  16928  ram0  16929  0ramcl  16930  gsumval2  18589  sgrp2nmndlem5  18832  issubg2  19049  ghmrn  19136  pmtrmvd  19363  gsumval3  19814  pgpfaclem2  19991  ablfaclem2  19995  ablfaclem3  19996  fincygsubgodd  20021  subdrgint  20713  abvdom  20740  lbsextlem2  21091  cndrng  21330  gzrngunit  21365  zringunit  21398  cnmsgnsubg  21509  frlmssuvc2  21727  mhpmulcl  22059  iinopn  22812  cnconn  23332  1stcfb  23355  dissnlocfin  23439  fbasrn  23794  fclscmpi  23939  alexsublem  23954  ustuqtop5  24155  cnextucn  24212  dscmet  24482  reperflem  24729  evth  24880  cmetcaulem  25210  iscmet3  25215  metsscmetcld  25237  cmetss  25238  bcthlem5  25250  bcth2  25252  mbflimsup  25589  itg1addlem4  25622  itg1climres  25637  itg2monolem1  25673  itg2i1fseq2  25679  tdeglem4  25987  deg1add  26030  deg1mul2  26041  deg1tm  26046  dgreq  26171  dgradd2  26196  dgrmul  26198  dgrmulc  26199  dgrcolem1  26201  plyrem  26235  facth  26236  fta1lem  26237  vieta1lem1  26240  vieta1lem2  26241  vieta1  26242  qaa  26253  aareccl  26256  geolim3  26269  aaliou3lem9  26280  coseq00topi  26433  cosne0  26460  tanord  26469  tanarg  26550  cxpne0  26608  cxpsqrt  26634  logbrec  26714  chordthmlem  26764  chordthmlem2  26765  dcubic  26778  mcubic  26779  cubic2  26780  cubic  26781  quartlem4  26792  atandmneg  26838  atandmcj  26841  atancj  26842  atanrecl  26843  atanlogsublem  26847  efiatan2  26849  tanatan  26851  atandmtan  26852  cosatan  26853  cosatanne0  26854  wilthlem2  27001  ftalem7  27011  basellem2  27014  basellem4  27016  basellem5  27017  isppw  27046  dchrptlem2  27198  lgsne0  27268  2sqlem8a  27358  2sqlem8  27359  noseponlem  27598  recsne0  28126  tglnpt2  28614  midexlem  28665  colperpexlem3  28705  mideulem2  28707  lnopp2hpgb  28736  subgruhgredgd  29257  wwlksnext  29866  wspthsnonn0vne  29890  clwwisshclwws  29987  vdn0conngrumgrv2  30168  vdgn1frgrv2  30268  nrt2irr  30445  ifnetrue  32519  ifnefals  32520  imadifxp  32573  acunirnmpt  32633  fnpreimac  32645  quad3d  32725  xaddeq0  32728  pmtrcnelor  33052  domnprodn0  33234  qsidomlem2  33410  ply1dg3rt0irred  33538  m1pmeq  33539  ply1annnr  33708  minplyirred  33716  rtelextdg2lem  33731  constrrtcclem  33739  constrconj  33750  constrext2chnlem  33755  constrremulcl  33772  constrrecl  33774  constrreinvcl  33777  2sqr3minply  33785  2sqr3nconstr  33786  cos9thpiminplylem1  33787  cos9thpiminplylem2  33788  cos9thpiminplylem3  33789  cos9thpiminply  33793  cos9thpinconstrlem1  33794  cos9thpinconstrlem2  33795  cos9thpinconstr  33796  madjusmdetlem2  33833  zar0ring  33883  xrge0iifhom  33942  signswn0  34565  signsvtn0  34575  signstfvneq0  34577  repr0  34616  derangenlem  35207  subfacp1lem3  35218  subfacp1lem5  35220  wsuclem  35859  ivthALT  36369  neibastop1  36393  weiunfrlem  36498  finxpreclem2  37424  finxpreclem6  37430  tan2h  37652  poimirlem9  37669  heicant  37695  itg2addnclem2  37712  lsatfixedN  39048  islshpat  39056  lkrshp  39144  2llnm3N  39608  dalemdnee  39705  cdleme18b  40331  cdleme40m  40506  cdlemg12g  40688  cdlemh  40856  cdlemj3  40862  tendoconid  40868  cdlemk3  40872  cdlemk12  40889  cdlemk12u  40911  cdlemk46  40987  cdlemk54  40997  erngdvlem4  41030  erngdvlem4-rN  41038  dibn0  41192  dihglblem2aN  41332  dochshpncl  41423  dochsnnz  41489  dochsatshpb  41491  lcfl7lem  41538  lcfl8b  41543  lcfrlem33  41614  lcfr  41624  hdmaprnlem3uN  41890  aks4d1p1p7  42107  fldhmf1  42123  primrootspoweq0  42139  idomnnzpownz  42165  idomnnzgmulnz  42166  aks6d1c5lem2  42171  deg1gprod  42173  unitscyglem4  42231  tanhalfpim  42382  remul01  42440  remulinvcom  42466  domnexpgn0cl  42556  ricdrng1  42561  prjcrv0  42666  3cubeslem2  42718  cmpfiiin  42730  pell1234qrne0  42886  rmxyneg  42953  fnwe2lem2  43084  kelac1  43096  wnefimgd  44194  radcnvrat  44347  binomcxplemfrat  44384  binomcxplemradcnv  44385  disjrnmpt2  45225  disjf1o  45228  choicefi  45237  ioondisj2  45533  ioondisj1  45534  lptioo2  45671  lptioo1  45672  0ellimcdiv  45687  liminflbuz2  45853  ioodvbdlimc1  45971  ioodvbdlimc2  45973  stoweidlem31  46069  stoweidlem59  46097  wallispilem4  46106  wallispi  46108  stirlinglem3  46114  stirlinglem14  46125  dirkerper  46134  dirkertrigeq  46139  dirkercncflem2  46142  fourierdlem4  46149  fourierdlem30  46175  fourierdlem41  46186  fourierdlem42  46187  fourierdlem44  46189  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem62  46206  fourierdlem74  46218  fourierdlem75  46219  fourierdlem79  46223  fourierdlem102  46246  fourierdlem114  46258  fouriersw  46269  elaa2lem  46271  elaa2  46272  etransclem24  46296  etransclem44  46316  etransclem47  46319  ioorrnopnlem  46342  subsaliuncl  46396  sge0cl  46419  meadjun  46500  meadjiunlem  46503  hoicvr  46586  ovnsubadd2lem  46683  smflimlem6  46814  smfpimcc  46846  smflimsuplem2  46859  cjnpoly  46920  modm2nep1  47397  modm1nep2  47399  modm1p1ne  47401  lswn0  47475  sprvalpwn0  47514  fmtnoprmfac1lem  47595  grimuhgr  47918  gpg3nbgrvtx0  48107  el0ldep  48498  islindeps2  48515  ldepsnlinclem1  48537  ldepsnlinclem2  48538  itscnhlinecirc02plem1  48814  fvconstr  48893  fvconstrn0  48894  catprs  49043  fucofvalne  49357