Theorem eqnetrd 3014

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

Syntax hints:   → wi 4   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  eqnetrrd  3015  3netr4d  3024  opnz  5493  xpdifid  6199  undefne0  8320  onoviun  8399  intrnfi  9485  cantnfp1lem2  9748  cantnfp1lem3  9749  wemapwe  9766  acndom2  10123  fin23lem14  10402  fin23lem40  10420  isf32lem6  10427  isf34lem5  10447  isf34lem7  10448  isf34lem6  10449  axcc2lem  10505  xaddnemnf  13298  xaddnepnf  13299  fseqsupcl  14028  hashprg  14444  elprchashprn2  14445  hash1n0  14470  limsupgre  15527  isercolllem3  15715  prodfn0  15942  ntrivcvgtail  15948  fproddiv  16009  fprodn0  16027  tanval3  16182  tanneg  16196  ruclem11  16288  nn0rppwr  16608  bezoutr1  16616  phibndlem  16817  dfphi2  16821  0ram  17067  0ram2  17068  ram0  17069  0ramcl  17070  gsumval2  18724  sgrp2nmndlem5  18964  issubg2  19181  ghmrn  19269  pmtrmvd  19498  gsumval3  19949  pgpfaclem2  20126  ablfaclem2  20130  ablfaclem3  20131  fincygsubgodd  20156  subdrgint  20826  abvdom  20853  lbsextlem2  21184  cndrng  21434  gzrngunit  21474  zringunit  21500  cnmsgnsubg  21618  frlmssuvc2  21838  mhpmulcl  22176  iinopn  22929  cnconn  23451  1stcfb  23474  dissnlocfin  23558  fbasrn  23913  fclscmpi  24058  alexsublem  24073  ustuqtop5  24275  cnextucn  24333  dscmet  24606  reperflem  24859  evth  25010  cmetcaulem  25341  iscmet3  25346  metsscmetcld  25368  cmetss  25369  bcthlem5  25381  bcth2  25383  mbflimsup  25720  itg1addlem4  25753  itg1addlem4OLD  25754  itg1climres  25769  itg2monolem1  25805  itg2i1fseq2  25811  tdeglem4  26119  deg1add  26162  deg1mul2  26173  deg1tm  26178  dgreq  26303  dgradd2  26328  dgrmul  26330  dgrmulc  26331  dgrcolem1  26333  plyrem  26365  facth  26366  fta1lem  26367  vieta1lem1  26370  vieta1lem2  26371  vieta1  26372  qaa  26383  aareccl  26386  geolim3  26399  aaliou3lem9  26410  coseq00topi  26562  cosne0  26589  tanord  26598  tanarg  26679  cxpne0  26737  cxpsqrt  26763  logbrec  26843  chordthmlem  26893  chordthmlem2  26894  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  quartlem4  26921  atandmneg  26967  atandmcj  26970  atancj  26971  atanrecl  26972  atanlogsublem  26976  efiatan2  26978  tanatan  26980  atandmtan  26981  cosatan  26982  cosatanne0  26983  wilthlem2  27130  ftalem7  27140  basellem2  27143  basellem4  27145  basellem5  27146  isppw  27175  dchrptlem2  27327  lgsne0  27397  2sqlem8a  27487  2sqlem8  27488  noseponlem  27727  tglnpt2  28667  midexlem  28718  colperpexlem3  28758  mideulem2  28760  lnopp2hpgb  28789  subgruhgredgd  29319  wwlksnext  29926  wspthsnonn0vne  29950  clwwisshclwws  30047  vdn0conngrumgrv2  30228  vdgn1frgrv2  30328  nrt2irr  30505  ifnetrue  32570  ifnefals  32571  imadifxp  32623  acunirnmpt  32677  fnpreimac  32689  quad3d  32757  xaddeq0  32760  pmtrcnelor  33084  domnprodn0  33247  qsidomlem2  33446  ply1dg3rt0irred  33572  m1pmeq  33573  ply1annnr  33696  minplyirred  33704  rtelextdg2lem  33717  constrrtcclem  33725  constrconj  33735  2sqr3minply  33738  madjusmdetlem2  33774  zar0ring  33824  xrge0iifhom  33883  signswn0  34537  signsvtn0  34547  signstfvneq0  34549  repr0  34588  derangenlem  35139  subfacp1lem3  35150  subfacp1lem5  35152  wsuclem  35789  ivthALT  36301  neibastop1  36325  weiunfrlem  36430  finxpreclem2  37356  finxpreclem6  37362  tan2h  37572  poimirlem9  37589  heicant  37615  itg2addnclem2  37632  lsatfixedN  38965  islshpat  38973  lkrshp  39061  2llnm3N  39526  dalemdnee  39623  cdleme18b  40249  cdleme40m  40424  cdlemg12g  40606  cdlemh  40774  cdlemj3  40780  tendoconid  40786  cdlemk3  40790  cdlemk12  40807  cdlemk12u  40829  cdlemk46  40905  cdlemk54  40915  erngdvlem4  40948  erngdvlem4-rN  40956  dibn0  41110  dihglblem2aN  41250  dochshpncl  41341  dochsnnz  41407  dochsatshpb  41409  lcfl7lem  41456  lcfl8b  41461  lcfrlem33  41532  lcfr  41542  hdmaprnlem3uN  41808  aks4d1p1p7  42031  fldhmf1  42047  primrootspoweq0  42063  idomnnzpownz  42089  idomnnzgmulnz  42090  aks6d1c5lem2  42095  deg1gprod  42097  unitscyglem4  42155  metakunt7  42168  tanhalfpim  42337  remul01  42383  remulinvcom  42408  domnexpgn0cl  42478  ricdrng1  42483  prjcrv0  42588  3cubeslem2  42641  cmpfiiin  42653  pell1234qrne0  42809  rmxyneg  42877  fnwe2lem2  43008  kelac1  43020  wnefimgd  44123  radcnvrat  44283  binomcxplemfrat  44320  binomcxplemradcnv  44321  disjrnmpt2  45095  disjf1o  45098  choicefi  45107  ioondisj2  45411  ioondisj1  45412  lptioo2  45552  lptioo1  45553  0ellimcdiv  45570  liminflbuz2  45736  ioodvbdlimc1  45854  ioodvbdlimc2  45856  stoweidlem31  45952  stoweidlem59  45980  wallispilem4  45989  wallispi  45991  stirlinglem3  45997  stirlinglem14  46008  dirkerper  46017  dirkertrigeq  46022  dirkercncflem2  46025  fourierdlem4  46032  fourierdlem30  46058  fourierdlem41  46069  fourierdlem42  46070  fourierdlem44  46072  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  fourierdlem79  46106  fourierdlem102  46129  fourierdlem114  46141  fouriersw  46152  elaa2lem  46154  elaa2  46155  etransclem24  46179  etransclem44  46199  etransclem47  46202  ioorrnopnlem  46225  subsaliuncl  46279  sge0cl  46302  meadjun  46383  meadjiunlem  46386  hoicvr  46469  ovnsubadd2lem  46566  smflimlem6  46697  smfpimcc  46729  smflimsuplem2  46742  lswn0  47318  sprvalpwn0  47357  fmtnoprmfac1lem  47438  grimuhgr  47762  el0ldep  48195  islindeps2  48212  ldepsnlinclem1  48234  ldepsnlinclem2  48235  itscnhlinecirc02plem1  48516  fvconstr  48569  fvconstrn0  48570  catprs  48678