Theorem eqnetrd 3000

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

Syntax hints:   → wi 4   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  eqnetrrd  3001  3netr4d  3010  opnz  5421  xpdifid  6126  undefne0  8222  onoviun  8276  intrnfi  9322  cantnfp1lem2  9591  cantnfp1lem3  9592  wemapwe  9609  acndom2  9967  fin23lem14  10246  fin23lem40  10264  isf32lem6  10271  isf34lem5  10291  isf34lem7  10292  isf34lem6  10293  axcc2lem  10349  xaddnemnf  13179  xaddnepnf  13180  fseqsupcl  13930  hashprg  14348  elprchashprn2  14349  hash1n0  14374  limsupgre  15434  isercolllem3  15620  prodfn0  15850  ntrivcvgtail  15856  fproddiv  15917  fprodn0  15935  tanval3  16092  tanneg  16106  ruclem11  16198  nn0rppwr  16521  bezoutr1  16529  phibndlem  16731  dfphi2  16735  0ram  16982  0ram2  16983  ram0  16984  0ramcl  16985  gsumval2  18645  sgrp2nmndlem5  18891  issubg2  19108  ghmrn  19195  pmtrmvd  19422  gsumval3  19873  pgpfaclem2  20050  ablfaclem2  20054  ablfaclem3  20055  fincygsubgodd  20080  subdrgint  20771  abvdom  20798  lbsextlem2  21149  cndrng  21388  gzrngunit  21423  zringunit  21456  cnmsgnsubg  21567  frlmssuvc2  21785  mhpmulcl  22125  iinopn  22877  cnconn  23397  1stcfb  23420  dissnlocfin  23504  fbasrn  23859  fclscmpi  24004  alexsublem  24019  ustuqtop5  24220  cnextucn  24277  dscmet  24547  reperflem  24794  evth  24936  cmetcaulem  25265  iscmet3  25270  metsscmetcld  25292  cmetss  25293  bcthlem5  25305  bcth2  25307  mbflimsup  25643  itg1addlem4  25676  itg1climres  25691  itg2monolem1  25727  itg2i1fseq2  25733  tdeglem4  26035  deg1add  26078  deg1mul2  26089  deg1tm  26094  dgreq  26219  dgradd2  26243  dgrmul  26245  dgrmulc  26246  dgrcolem1  26248  plyrem  26282  facth  26283  fta1lem  26284  vieta1lem1  26287  vieta1lem2  26288  vieta1  26289  qaa  26300  aareccl  26303  geolim3  26316  aaliou3lem9  26327  coseq00topi  26479  cosne0  26506  tanord  26515  tanarg  26596  cxpne0  26654  cxpsqrt  26680  logbrec  26759  chordthmlem  26809  chordthmlem2  26810  dcubic  26823  mcubic  26824  cubic2  26825  cubic  26826  quartlem4  26837  atandmneg  26883  atandmcj  26886  atancj  26887  atanrecl  26888  atanlogsublem  26892  efiatan2  26894  tanatan  26896  atandmtan  26897  cosatan  26898  cosatanne0  26899  wilthlem2  27046  ftalem7  27056  basellem2  27059  basellem4  27061  basellem5  27062  isppw  27091  dchrptlem2  27242  lgsne0  27312  2sqlem8a  27402  2sqlem8  27403  noseponlem  27642  recsne0  28198  tglnpt2  28723  midexlem  28774  colperpexlem3  28814  mideulem2  28816  lnopp2hpgb  28845  subgruhgredgd  29367  wwlksnext  29976  wspthsnonn0vne  30000  clwwisshclwws  30100  vdn0conngrumgrv2  30281  vdgn1frgrv2  30381  nrt2irr  30558  ifnetrue  32632  ifnefals  32633  imadifxp  32686  acunirnmpt  32747  fnpreimac  32758  quad3d  32837  xaddeq0  32841  pmtrcnelor  33167  domnprodn0  33351  domnprodeq0  33352  qsidomlem2  33528  ply1dg3rt0irred  33659  m1pmeq  33660  mplmulmvr  33698  esplyfvaln  33733  esplyind  33734  ply1annnr  33863  minplyirred  33871  rtelextdg2lem  33886  constrrtcclem  33894  constrconj  33905  constrext2chnlem  33910  constrremulcl  33927  constrrecl  33929  constrreinvcl  33932  2sqr3minply  33940  2sqr3nconstr  33941  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  cos9thpiminplylem3  33944  cos9thpiminply  33948  cos9thpinconstrlem1  33949  cos9thpinconstrlem2  33950  cos9thpinconstr  33951  madjusmdetlem2  33988  zar0ring  34038  xrge0iifhom  34097  signswn0  34720  signsvtn0  34730  signstfvneq0  34732  repr0  34771  derangenlem  35369  subfacp1lem3  35380  subfacp1lem5  35382  wsuclem  36021  ivthALT  36533  neibastop1  36557  weiunfrlem  36662  finxpreclem2  37720  finxpreclem6  37726  tan2h  37947  poimirlem9  37964  heicant  37990  itg2addnclem2  38007  lsatfixedN  39469  islshpat  39477  lkrshp  39565  2llnm3N  40029  dalemdnee  40126  cdleme18b  40752  cdleme40m  40927  cdlemg12g  41109  cdlemh  41277  cdlemj3  41283  tendoconid  41289  cdlemk3  41293  cdlemk12  41310  cdlemk12u  41332  cdlemk46  41408  cdlemk54  41418  erngdvlem4  41451  erngdvlem4-rN  41459  dibn0  41613  dihglblem2aN  41753  dochshpncl  41844  dochsnnz  41910  dochsatshpb  41912  lcfl7lem  41959  lcfl8b  41964  lcfrlem33  42035  lcfr  42045  hdmaprnlem3uN  42311  aks4d1p1p7  42527  fldhmf1  42543  primrootspoweq0  42559  idomnnzpownz  42585  idomnnzgmulnz  42586  aks6d1c5lem2  42591  deg1gprod  42593  unitscyglem4  42651  tanhalfpim  42795  remul01  42853  remulinvcom  42879  domnexpgn0cl  42982  ricdrng1  42987  prjcrv0  43080  3cubeslem2  43131  cmpfiiin  43143  pell1234qrne0  43299  rmxyneg  43366  fnwe2lem2  43497  kelac1  43509  wnefimgd  44606  radcnvrat  44759  binomcxplemfrat  44796  binomcxplemradcnv  44797  disjrnmpt2  45636  disjf1o  45639  choicefi  45647  ioondisj2  45941  ioondisj1  45942  lptioo2  46079  lptioo1  46080  0ellimcdiv  46095  liminflbuz2  46261  ioodvbdlimc1  46379  ioodvbdlimc2  46381  stoweidlem31  46477  stoweidlem59  46505  wallispilem4  46514  wallispi  46516  stirlinglem3  46522  stirlinglem14  46533  dirkerper  46542  dirkertrigeq  46547  dirkercncflem2  46550  fourierdlem4  46557  fourierdlem30  46583  fourierdlem41  46594  fourierdlem42  46595  fourierdlem44  46597  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem62  46614  fourierdlem74  46626  fourierdlem75  46627  fourierdlem79  46631  fourierdlem102  46654  fourierdlem114  46666  fouriersw  46677  elaa2lem  46679  elaa2  46680  etransclem24  46704  etransclem44  46724  etransclem47  46727  ioorrnopnlem  46750  subsaliuncl  46804  sge0cl  46827  meadjun  46908  meadjiunlem  46911  hoicvr  46994  ovnsubadd2lem  47091  smflimlem6  47222  smfpimcc  47254  smflimsuplem2  47267  cjnpoly  47349  modm2nep1  47832  modm1nep2  47834  modm1p1ne  47836  lswn0  47916  sprvalpwn0  47955  fmtnoprmfac1lem  48039  grimuhgr  48375  gpg3nbgrvtx0  48564  el0ldep  48954  islindeps2  48971  ldepsnlinclem1  48993  ldepsnlinclem2  48994  itscnhlinecirc02plem1  49270  fvconstr  49349  fvconstrn0  49350  catprs  49498  fucofvalne  49812