Theorem eqnetrd 3028

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

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

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 2738

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

This theorem is used by:  eqnetrrd  3029  3netr4d  3038  opnz  5460  xpdifid  6170  undefne0  8285  onoviun  8339  intrnfi  9386  cantnfp1lem2  9658  cantnfp1lem3  9659  wemapwe  9676  acndom2  10057  fin23lem14  10335  fin23lem40  10353  isf32lem6  10360  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  axcc2lem  10438  xaddnemnf  13280  xaddnepnf  13281  fseqsupcl  14033  hashprg  14451  elprchashprn2  14452  hash1n0  14478  limsupgre  15558  isercolllem3  15744  prodfn0  15974  ntrivcvgtail  15980  fproddiv  16041  fprodn0  16059  tanval3  16215  tanneg  16229  ruclem11  16321  nn0rppwr  16644  bezoutr1  16652  phibndlem  16854  dfphi2  16858  0ram  17105  0ram2  17106  ram0  17107  0ramcl  17108  gsumval2  18769  sgrp2nmndlem5  19016  issubg2  19233  ghmrn  19324  pmtrmvd  19551  gsumval3  20002  pgpfaclem2  20179  ablfaclem2  20183  ablfaclem3  20184  fincygsubgodd  20209  subdrgint  20936  abvdom  20963  lbsextlem2  21313  qsidomlem2  21511  cndrng  21581  gzrngunit  21613  zringunit  21646  cnmsgnsubg  21757  frlmssuvc2  21975  mhpmulcl  22342  iinopn  23089  cnconn  23609  1stcfb  23632  dissnlocfin  23716  fbasrn  24071  fclscmpi  24216  alexsublem  24231  ustuqtop5  24432  cnextucn  24489  dscmet  24759  reperflem  25006  evth  25148  cmetcaulem  25477  iscmet3  25482  metsscmetcld  25504  cmetss  25505  bcthlem5  25517  bcth2  25519  mbflimsup  25855  itg1addlem4  25888  itg1climres  25903  itg2monolem1  25939  itg2i1fseq2  25945  tdeglem4  26247  deg1add  26290  deg1mul2  26301  deg1tm  26306  dgreq  26431  dgradd2  26455  dgrmul  26457  dgrmulc  26458  dgrcolem1  26460  plyrem  26496  facth  26497  fta1lem  26498  vieta1lem1  26501  vieta1lem2  26502  vieta1  26503  qaa  26514  aareccl  26519  geolim3  26532  aaliou3lem9  26543  coseq00topi  26697  cosne0  26724  tanord  26733  tanarg  26814  cxpne0  26872  cxpsqrt  26898  logbrec  26977  chordthmlem  27027  chordthmlem2  27028  dcubic  27041  mcubic  27042  cubic2  27043  cubic  27044  quartlem4  27055  atandmneg  27101  atandmcj  27104  atancj  27105  atanrecl  27106  atanlogsublem  27110  efiatan2  27112  tanatan  27114  atandmtan  27115  cosatan  27116  cosatanne0  27117  wilthlem2  27263  ftalem7  27273  basellem2  27276  basellem4  27278  basellem5  27279  isppw  27308  dchrptlem2  27459  lgsne0  27529  2sqlem8a  27619  2sqlem8  27620  noseponlem  27858  recsne0  28415  tglnpt2  28956  midexlem  28999  colperpexlem3  29043  mideulem2  29045  lnopp2hpgb  29075  subgruhgredgd  29664  wwlksnext  30272  wspthsnonn0vne  30296  clwwisshclwws  30396  vdn0conngrumgrv2  30577  vdgn1frgrv2  30677  nrt2irr  30854  ifnetrue  32923  ifnefals  32924  imadifxp  32976  acunirnmpt  33034  fnpreimac  33045  quad3d  33124  xaddeq0  33128  pmtrcnelor  33435  domnprodn0  33622  domnprodeq0  33623  drnglring  33806  dflringlem3  33810  dflring4  33812  ply1dg3rt0irred  33898  m1pmeq  33899  mplmulmvr  33953  esplyfvaln  33988  esplyind  33989  ply1annnr  34117  minplyirred  34125  rtelextdg2lem  34140  constrrtcclem  34148  constrconj  34159  constrext2chnlem  34164  constrremulcl  34181  constrrecl  34183  constrreinvcl  34186  2sqr3minply  34194  2sqr3nconstr  34195  cos9thpiminplylem1  34196  cos9thpiminplylem2  34197  cos9thpiminplylem3  34198  cos9thpiminply  34202  cos9thpinconstrlem1  34203  cos9thpinconstrlem2  34204  cos9thpinconstr  34205  madjusmdetlem2  34242  zar0ring  34292  xrge0iifhom  34351  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