Theorem eqnetrd 2999

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

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

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 2708

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

This theorem is referenced by:  eqnetrrd  3000  3netr4d  3009  opnz  5426  xpdifid  6132  undefne0  8229  onoviun  8283  intrnfi  9329  cantnfp1lem2  9600  cantnfp1lem3  9601  wemapwe  9618  acndom2  9976  fin23lem14  10255  fin23lem40  10273  isf32lem6  10280  isf34lem5  10300  isf34lem7  10301  isf34lem6  10302  axcc2lem  10358  xaddnemnf  13188  xaddnepnf  13189  fseqsupcl  13939  hashprg  14357  elprchashprn2  14358  hash1n0  14383  limsupgre  15443  isercolllem3  15629  prodfn0  15859  ntrivcvgtail  15865  fproddiv  15926  fprodn0  15944  tanval3  16101  tanneg  16115  ruclem11  16207  nn0rppwr  16530  bezoutr1  16538  phibndlem  16740  dfphi2  16744  0ram  16991  0ram2  16992  ram0  16993  0ramcl  16994  gsumval2  18654  sgrp2nmndlem5  18900  issubg2  19117  ghmrn  19204  pmtrmvd  19431  gsumval3  19882  pgpfaclem2  20059  ablfaclem2  20063  ablfaclem3  20064  fincygsubgodd  20089  subdrgint  20780  abvdom  20807  lbsextlem2  21157  cndrng  21381  gzrngunit  21413  zringunit  21446  cnmsgnsubg  21557  frlmssuvc2  21775  mhpmulcl  22115  iinopn  22867  cnconn  23387  1stcfb  23410  dissnlocfin  23494  fbasrn  23849  fclscmpi  23994  alexsublem  24009  ustuqtop5  24210  cnextucn  24267  dscmet  24537  reperflem  24784  evth  24926  cmetcaulem  25255  iscmet3  25260  metsscmetcld  25282  cmetss  25283  bcthlem5  25295  bcth2  25297  mbflimsup  25633  itg1addlem4  25666  itg1climres  25681  itg2monolem1  25717  itg2i1fseq2  25723  tdeglem4  26025  deg1add  26068  deg1mul2  26079  deg1tm  26084  dgreq  26209  dgradd2  26233  dgrmul  26235  dgrmulc  26236  dgrcolem1  26238  plyrem  26271  facth  26272  fta1lem  26273  vieta1lem1  26276  vieta1lem2  26277  vieta1  26278  qaa  26289  aareccl  26292  geolim3  26305  aaliou3lem9  26316  coseq00topi  26466  cosne0  26493  tanord  26502  tanarg  26583  cxpne0  26641  cxpsqrt  26667  logbrec  26746  chordthmlem  26796  chordthmlem2  26797  dcubic  26810  mcubic  26811  cubic2  26812  cubic  26813  quartlem4  26824  atandmneg  26870  atandmcj  26873  atancj  26874  atanrecl  26875  atanlogsublem  26879  efiatan2  26881  tanatan  26883  atandmtan  26884  cosatan  26885  cosatanne0  26886  wilthlem2  27032  ftalem7  27042  basellem2  27045  basellem4  27047  basellem5  27048  isppw  27077  dchrptlem2  27228  lgsne0  27298  2sqlem8a  27388  2sqlem8  27389  noseponlem  27628  recsne0  28184  tglnpt2  28709  midexlem  28760  colperpexlem3  28800  mideulem2  28802  lnopp2hpgb  28831  subgruhgredgd  29353  wwlksnext  29961  wspthsnonn0vne  29985  clwwisshclwws  30085  vdn0conngrumgrv2  30266  vdgn1frgrv2  30366  nrt2irr  30543  ifnetrue  32617  ifnefals  32618  imadifxp  32671  acunirnmpt  32732  fnpreimac  32743  quad3d  32822  xaddeq0  32826  pmtrcnelor  33152  domnprodn0  33336  domnprodeq0  33337  qsidomlem2  33513  ply1dg3rt0irred  33644  m1pmeq  33645  mplmulmvr  33683  esplyfvaln  33718  esplyind  33719  ply1annnr  33847  minplyirred  33855  rtelextdg2lem  33870  constrrtcclem  33878  constrconj  33889  constrext2chnlem  33894  constrremulcl  33911  constrrecl  33913  constrreinvcl  33916  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminply  33932  cos9thpinconstrlem1  33933  cos9thpinconstrlem2  33934  cos9thpinconstr  33935  madjusmdetlem2  33972  zar0ring  34022  xrge0iifhom  34081  signswn0  34704  signsvtn0  34714  signstfvneq0  34716  repr0  34755  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  wsuclem  36005  ivthALT  36517  neibastop1  36541  weiunfrlem  36646  finxpreclem2  37706  finxpreclem6  37712  tan2h  37933  poimirlem9  37950  heicant  37976  itg2addnclem2  37993  lsatfixedN  39455  islshpat  39463  lkrshp  39551  2llnm3N  40015  dalemdnee  40112  cdleme18b  40738  cdleme40m  40913  cdlemg12g  41095  cdlemh  41263  cdlemj3  41269  tendoconid  41275  cdlemk3  41279  cdlemk12  41296  cdlemk12u  41318  cdlemk46  41394  cdlemk54  41404  erngdvlem4  41437  erngdvlem4-rN  41445  dibn0  41599  dihglblem2aN  41739  dochshpncl  41830  dochsnnz  41896  dochsatshpb  41898  lcfl7lem  41945  lcfl8b  41950  lcfrlem33  42021  lcfr  42031  hdmaprnlem3uN  42297  aks4d1p1p7  42513  fldhmf1  42529  primrootspoweq0  42545  idomnnzpownz  42571  idomnnzgmulnz  42572  aks6d1c5lem2  42577  deg1gprod  42579  unitscyglem4  42637  tanhalfpim  42781  remul01  42839  remulinvcom  42865  domnexpgn0cl  42968  ricdrng1  42973  prjcrv0  43066  3cubeslem2  43117  cmpfiiin  43129  pell1234qrne0  43281  rmxyneg  43348  fnwe2lem2  43479  kelac1  43491  wnefimgd  44588  radcnvrat  44741  binomcxplemfrat  44778  binomcxplemradcnv  44779  disjrnmpt2  45618  disjf1o  45621  choicefi  45629  ioondisj2  45923  ioondisj1  45924  lptioo2  46061  lptioo1  46062  0ellimcdiv  46077  liminflbuz2  46243  ioodvbdlimc1  46361  ioodvbdlimc2  46363  stoweidlem31  46459  stoweidlem59  46487  wallispilem4  46496  wallispi  46498  stirlinglem3  46504  stirlinglem14  46515  dirkerper  46524  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem4  46539  fourierdlem30  46565  fourierdlem41  46576  fourierdlem42  46577  fourierdlem44  46579  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem102  46636  fourierdlem114  46648  fouriersw  46659  elaa2lem  46661  elaa2  46662  etransclem24  46686  etransclem44  46706  etransclem47  46709  ioorrnopnlem  46732  subsaliuncl  46786  sge0cl  46809  meadjun  46890  meadjiunlem  46893  hoicvr  46976  ovnsubadd2lem  47073  smflimlem6  47204  smfpimcc  47236  smflimsuplem2  47249  cjnpoly  47337  modm2nep1  47820  modm1nep2  47822  modm1p1ne  47824  lswn0  47904  sprvalpwn0  47943  fmtnoprmfac1lem  48027  grimuhgr  48363  gpg3nbgrvtx0  48552  el0ldep  48942  islindeps2  48959  ldepsnlinclem1  48981  ldepsnlinclem2  48982  itscnhlinecirc02plem1  49258  fvconstr  49337  fvconstrn0  49338  catprs  49486  fucofvalne  49800