Theorem eqnetrd 2992

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

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrrd  2993  3netr4d  3002  opnz  5428  xpdifid  6129  undefne0  8235  onoviun  8289  intrnfi  9343  cantnfp1lem2  9608  cantnfp1lem3  9609  wemapwe  9626  acndom2  9983  fin23lem14  10262  fin23lem40  10280  isf32lem6  10287  isf34lem5  10307  isf34lem7  10308  isf34lem6  10309  axcc2lem  10365  xaddnemnf  13172  xaddnepnf  13173  fseqsupcl  13918  hashprg  14336  elprchashprn2  14337  hash1n0  14362  limsupgre  15423  isercolllem3  15609  prodfn0  15836  ntrivcvgtail  15842  fproddiv  15903  fprodn0  15921  tanval3  16078  tanneg  16092  ruclem11  16184  nn0rppwr  16507  bezoutr1  16515  phibndlem  16716  dfphi2  16720  0ram  16967  0ram2  16968  ram0  16969  0ramcl  16970  gsumval2  18589  sgrp2nmndlem5  18832  issubg2  19049  ghmrn  19137  pmtrmvd  19362  gsumval3  19813  pgpfaclem2  19990  ablfaclem2  19994  ablfaclem3  19995  fincygsubgodd  20020  subdrgint  20688  abvdom  20715  lbsextlem2  21045  cndrng  21286  gzrngunit  21326  zringunit  21352  cnmsgnsubg  21462  frlmssuvc2  21680  mhpmulcl  22012  iinopn  22765  cnconn  23285  1stcfb  23308  dissnlocfin  23392  fbasrn  23747  fclscmpi  23892  alexsublem  23907  ustuqtop5  24109  cnextucn  24166  dscmet  24436  reperflem  24683  evth  24834  cmetcaulem  25164  iscmet3  25169  metsscmetcld  25191  cmetss  25192  bcthlem5  25204  bcth2  25206  mbflimsup  25543  itg1addlem4  25576  itg1climres  25591  itg2monolem1  25627  itg2i1fseq2  25633  tdeglem4  25941  deg1add  25984  deg1mul2  25995  deg1tm  26000  dgreq  26125  dgradd2  26150  dgrmul  26152  dgrmulc  26153  dgrcolem1  26155  plyrem  26189  facth  26190  fta1lem  26191  vieta1lem1  26194  vieta1lem2  26195  vieta1  26196  qaa  26207  aareccl  26210  geolim3  26223  aaliou3lem9  26234  coseq00topi  26387  cosne0  26414  tanord  26423  tanarg  26504  cxpne0  26562  cxpsqrt  26588  logbrec  26668  chordthmlem  26718  chordthmlem2  26719  dcubic  26732  mcubic  26733  cubic2  26734  cubic  26735  quartlem4  26746  atandmneg  26792  atandmcj  26795  atancj  26796  atanrecl  26797  atanlogsublem  26801  efiatan2  26803  tanatan  26805  atandmtan  26806  cosatan  26807  cosatanne0  26808  wilthlem2  26955  ftalem7  26965  basellem2  26968  basellem4  26970  basellem5  26971  isppw  27000  dchrptlem2  27152  lgsne0  27222  2sqlem8a  27312  2sqlem8  27313  noseponlem  27552  recsne0  28071  tglnpt2  28544  midexlem  28595  colperpexlem3  28635  mideulem2  28637  lnopp2hpgb  28666  subgruhgredgd  29187  wwlksnext  29796  wspthsnonn0vne  29820  clwwisshclwws  29917  vdn0conngrumgrv2  30098  vdgn1frgrv2  30198  nrt2irr  30375  ifnetrue  32449  ifnefals  32450  imadifxp  32503  acunirnmpt  32556  fnpreimac  32568  quad3d  32646  xaddeq0  32649  pmtrcnelor  33021  domnprodn0  33199  qsidomlem2  33397  ply1dg3rt0irred  33524  m1pmeq  33525  ply1annnr  33666  minplyirred  33674  rtelextdg2lem  33689  constrrtcclem  33697  constrconj  33708  constrext2chnlem  33713  constrremulcl  33730  constrrecl  33732  constrreinvcl  33735  2sqr3minply  33743  2sqr3nconstr  33744  cos9thpiminplylem1  33745  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminply  33751  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  cos9thpinconstr  33754  madjusmdetlem2  33791  zar0ring  33841  xrge0iifhom  33900  signswn0  34524  signsvtn0  34534  signstfvneq0  34536  repr0  34575  derangenlem  35131  subfacp1lem3  35142  subfacp1lem5  35144  wsuclem  35786  ivthALT  36296  neibastop1  36320  weiunfrlem  36425  finxpreclem2  37351  finxpreclem6  37357  tan2h  37579  poimirlem9  37596  heicant  37622  itg2addnclem2  37639  lsatfixedN  38975  islshpat  38983  lkrshp  39071  2llnm3N  39536  dalemdnee  39633  cdleme18b  40259  cdleme40m  40434  cdlemg12g  40616  cdlemh  40784  cdlemj3  40790  tendoconid  40796  cdlemk3  40800  cdlemk12  40817  cdlemk12u  40839  cdlemk46  40915  cdlemk54  40925  erngdvlem4  40958  erngdvlem4-rN  40966  dibn0  41120  dihglblem2aN  41260  dochshpncl  41351  dochsnnz  41417  dochsatshpb  41419  lcfl7lem  41466  lcfl8b  41471  lcfrlem33  41542  lcfr  41552  hdmaprnlem3uN  41818  aks4d1p1p7  42035  fldhmf1  42051  primrootspoweq0  42067  idomnnzpownz  42093  idomnnzgmulnz  42094  aks6d1c5lem2  42099  deg1gprod  42101  unitscyglem4  42159  tanhalfpim  42310  remul01  42368  remulinvcom  42394  domnexpgn0cl  42484  ricdrng1  42489  prjcrv0  42594  3cubeslem2  42646  cmpfiiin  42658  pell1234qrne0  42814  rmxyneg  42882  fnwe2lem2  43013  kelac1  43025  wnefimgd  44123  radcnvrat  44276  binomcxplemfrat  44313  binomcxplemradcnv  44314  disjrnmpt2  45155  disjf1o  45158  choicefi  45167  ioondisj2  45464  ioondisj1  45465  lptioo2  45602  lptioo1  45603  0ellimcdiv  45620  liminflbuz2  45786  ioodvbdlimc1  45904  ioodvbdlimc2  45906  stoweidlem31  46002  stoweidlem59  46030  wallispilem4  46039  wallispi  46041  stirlinglem3  46047  stirlinglem14  46058  dirkerper  46067  dirkertrigeq  46072  dirkercncflem2  46075  fourierdlem4  46082  fourierdlem30  46108  fourierdlem41  46119  fourierdlem42  46120  fourierdlem44  46122  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem62  46139  fourierdlem74  46151  fourierdlem75  46152  fourierdlem79  46156  fourierdlem102  46179  fourierdlem114  46191  fouriersw  46202  elaa2lem  46204  elaa2  46205  etransclem24  46229  etransclem44  46249  etransclem47  46252  ioorrnopnlem  46275  subsaliuncl  46329  sge0cl  46352  meadjun  46433  meadjiunlem  46436  hoicvr  46519  ovnsubadd2lem  46616  smflimlem6  46747  smfpimcc  46779  smflimsuplem2  46792  cjnpoly  46863  modm2nep1  47340  modm1nep2  47342  modm1p1ne  47344  lswn0  47418  sprvalpwn0  47457  fmtnoprmfac1lem  47538  grimuhgr  47860  gpg3nbgrvtx0  48040  el0ldep  48428  islindeps2  48445  ldepsnlinclem1  48467  ldepsnlinclem2  48468  itscnhlinecirc02plem1  48744  fvconstr  48823  fvconstrn0  48824  catprs  48973  fucofvalne  49287