Theorem eqnetrd 3010

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  eqnetrrd  3011  3netr4d  3020  opnz  5382  xpdifid  6060  undefne0  8066  onoviun  8145  intrnfi  9105  cantnfp1lem2  9367  cantnfp1lem3  9368  wemapwe  9385  acndom2  9741  fin23lem14  10020  fin23lem40  10038  isf32lem6  10045  isf34lem5  10065  isf34lem7  10066  isf34lem6  10067  axcc2lem  10123  xaddnemnf  12899  xaddnepnf  12900  fseqsupcl  13625  hashprg  14038  elprchashprn2  14039  hash1n0  14064  limsupgre  15118  isercolllem3  15306  prodfn0  15534  ntrivcvgtail  15540  fproddiv  15599  fprodn0  15617  tanval3  15771  tanneg  15785  ruclem11  15877  bezoutr1  16202  phibndlem  16399  dfphi2  16403  0ram  16649  0ram2  16650  ram0  16651  0ramcl  16652  gsumval2  18285  sgrp2nmndlem5  18483  issubg2  18685  ghmrn  18762  pmtrmvd  18979  gsumval3  19423  pgpfaclem2  19600  ablfaclem2  19604  ablfaclem3  19605  fincygsubgodd  19630  subdrgint  19986  abvdom  20013  lbsextlem2  20336  gzrngunit  20576  zringunit  20600  cnmsgnsubg  20694  frlmssuvc2  20912  mhpmulcl  21249  iinopn  21959  cnconn  22481  1stcfb  22504  dissnlocfin  22588  fbasrn  22943  fclscmpi  23088  alexsublem  23103  ustuqtop5  23305  cnextucn  23363  dscmet  23634  reperflem  23887  evth  24028  cmetcaulem  24357  iscmet3  24362  metsscmetcld  24384  cmetss  24385  bcthlem5  24397  bcth2  24399  mbflimsup  24735  itg1addlem4  24768  itg1addlem4OLD  24769  itg1climres  24784  itg2monolem1  24820  itg2i1fseq2  24826  tdeglem4  25129  tdeglem4OLD  25130  deg1add  25173  deg1mul2  25184  deg1tm  25188  dgreq  25310  dgradd2  25334  dgrmul  25336  dgrmulc  25337  dgrcolem1  25339  plyrem  25370  facth  25371  fta1lem  25372  vieta1lem1  25375  vieta1lem2  25376  vieta1  25377  qaa  25388  aareccl  25391  geolim3  25404  aaliou3lem9  25415  coseq00topi  25564  cosne0  25590  tanord  25599  tanarg  25679  cxpne0  25737  cxpsqrt  25763  logbrec  25837  chordthmlem  25887  chordthmlem2  25888  dcubic  25901  mcubic  25902  cubic2  25903  cubic  25904  quartlem4  25915  atandmneg  25961  atandmcj  25964  atancj  25965  atanrecl  25966  atanlogsublem  25970  efiatan2  25972  tanatan  25974  atandmtan  25975  cosatan  25976  cosatanne0  25977  wilthlem2  26123  ftalem7  26133  basellem2  26136  basellem4  26138  basellem5  26139  isppw  26168  dchrptlem2  26318  lgsne0  26388  2sqlem8a  26478  2sqlem8  26479  tglnpt2  26906  midexlem  26957  colperpexlem3  26997  mideulem2  26999  lnopp2hpgb  27028  subgruhgredgd  27554  wwlksnext  28159  wspthsnonn0vne  28183  clwwisshclwws  28280  vdn0conngrumgrv2  28461  vdgn1frgrv2  28561  imadifxp  30841  acunirnmpt  30898  fnpreimac  30910  xaddeq0  30978  pmtrcnelor  31262  qsidomlem2  31531  madjusmdetlem2  31680  zar0ring  31730  xrge0iifhom  31789  signswn0  32439  signsvtn0  32449  signstfvneq0  32451  repr0  32491  derangenlem  33033  subfacp1lem3  33044  subfacp1lem5  33046  wsuclem  33746  noseponlem  33794  ivthALT  34451  neibastop1  34475  finxpreclem2  35488  finxpreclem6  35494  tan2h  35696  poimirlem9  35713  heicant  35739  itg2addnclem2  35756  lsatfixedN  36950  islshpat  36958  lkrshp  37046  2llnm3N  37510  dalemdnee  37607  cdleme18b  38233  cdleme40m  38408  cdlemg12g  38590  cdlemh  38758  cdlemj3  38764  tendoconid  38770  cdlemk3  38774  cdlemk12  38791  cdlemk12u  38813  cdlemk46  38889  cdlemk54  38899  erngdvlem4  38932  erngdvlem4-rN  38940  dibn0  39094  dihglblem2aN  39234  dochshpncl  39325  dochsnnz  39391  dochsatshpb  39393  lcfl7lem  39440  lcfl8b  39445  lcfrlem33  39516  lcfr  39526  hdmaprnlem3uN  39792  aks4d1p1p7  40010  metakunt7  40059  nn0rppwr  40254  remul01  40311  remulinvcom  40335  3cubeslem2  40423  cmpfiiin  40435  pell1234qrne0  40591  rmxyneg  40658  fnwe2lem2  40792  kelac1  40804  wnefimgd  41661  radcnvrat  41821  binomcxplemfrat  41858  binomcxplemradcnv  41859  disjrnmpt2  42615  disjf1o  42618  choicefi  42629  ioondisj2  42921  ioondisj1  42922  lptioo2  43062  lptioo1  43063  0ellimcdiv  43080  liminflbuz2  43246  ioodvbdlimc1  43364  ioodvbdlimc2  43366  stoweidlem31  43462  stoweidlem59  43490  wallispilem4  43499  wallispi  43501  stirlinglem3  43507  stirlinglem14  43518  dirkerper  43527  dirkertrigeq  43532  dirkercncflem2  43535  fourierdlem4  43542  fourierdlem30  43568  fourierdlem41  43579  fourierdlem42  43580  fourierdlem44  43582  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem62  43599  fourierdlem74  43611  fourierdlem75  43612  fourierdlem79  43616  fourierdlem102  43639  fourierdlem114  43651  fouriersw  43662  elaa2lem  43664  elaa2  43665  etransclem24  43689  etransclem44  43709  etransclem47  43712  ioorrnopnlem  43735  subsaliuncl  43787  sge0cl  43809  meadjun  43890  meadjiunlem  43893  hoicvr  43976  ovnsubadd2lem  44073  smflimlem6  44198  smfpimcc  44228  smflimsuplem2  44241  lswn0  44784  sprvalpwn0  44823  fmtnoprmfac1lem  44904  el0ldep  45695  islindeps2  45712  ldepsnlinclem1  45734  ldepsnlinclem2  45735  itscnhlinecirc02plem1  46016  fvconstr  46071  fvconstrn0  46072  catprs  46180