Theorem eqnetrd 3036

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

Syntax hints:   → wi 4   = wceq 1601   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-ne 2970

This theorem is referenced by:  eqnetrrd  3037  3netr4d  3046  opnz  5173  xpdifid  5816  undefne0  7687  onoviun  7723  intrnfi  8610  cantnfp1lem2  8873  cantnfp1lem3  8874  wemapwe  8891  acndom2  9210  fin23lem14  9490  fin23lem40  9508  isf32lem6  9515  isf34lem5  9535  isf34lem7  9536  isf34lem6  9537  axcc2lem  9593  xaddnemnf  12379  xaddnepnf  12380  fseqsupcl  13095  hashprg  13497  elprchashprn2  13498  hash1n0  13523  limsupgre  14620  isercolllem3  14805  prodfn0  15029  ntrivcvgtail  15035  fproddiv  15094  fprodn0  15112  tanval3  15266  tanneg  15280  ruclem11  15373  bezoutr1  15688  phibndlem  15879  dfphi2  15883  0ram  16128  0ram2  16129  ram0  16130  0ramcl  16131  gsumval2  17666  sgrp2nmndlem5  17803  issubg2  17993  ghmrn  18057  pmtrmvd  18259  gsumval3  18694  pgpfaclem2  18868  ablfaclem2  18872  ablfaclem3  18873  abvdom  19230  lbsextlem2  19556  gzrngunit  20208  zringunit  20232  cnmsgnsubg  20318  frlmssuvc2  20538  iinopn  21114  cnconn  21634  1stcfb  21657  dissnlocfin  21741  fbasrn  22096  fclscmpi  22241  alexsublem  22256  ustuqtop5  22457  cnextucn  22515  dscmet  22785  reperflem  23029  evth  23166  cmetcaulem  23494  iscmet3  23499  metsscmetcld  23521  cmetss  23522  bcthlem5  23534  bcth2  23536  mbflimsup  23870  itg1addlem4  23903  itg1climres  23918  itg2monolem1  23954  itg2i1fseq2  23960  tdeglem4  24257  deg1add  24300  deg1mul2  24311  deg1tm  24315  dgreq  24437  dgradd2  24461  dgrmul  24463  dgrmulc  24464  dgrcolem1  24466  plyrem  24497  facth  24498  fta1lem  24499  vieta1lem1  24502  vieta1lem2  24503  vieta1  24504  qaa  24515  aareccl  24518  geolim3  24531  aaliou3lem9  24542  coseq00topi  24692  cosne0  24714  tanord  24722  tanarg  24802  cxpne0  24860  cxpsqrt  24886  logbrec  24960  chordthmlem  25010  chordthmlem2  25011  dcubic  25024  mcubic  25025  cubic2  25026  cubic  25027  quartlem4  25038  atandmneg  25084  atandmcj  25087  atancj  25088  atanrecl  25089  atanlogsublem  25093  efiatan2  25095  tanatan  25097  atandmtan  25098  cosatan  25099  cosatanne0  25100  wilthlem2  25247  ftalem7  25257  basellem2  25260  basellem4  25262  basellem5  25263  isppw  25292  dchrptlem2  25442  lgsne0  25512  2sqlem8a  25602  2sqlem8  25603  tglnpt2  25992  midexlem  26043  colperpexlem3  26080  mideulem2  26082  lnopp2hpgb  26111  subgruhgredgd  26631  wwlksnext  27254  wspthsnonn0vne  27297  clwwisshclwws  27404  vdn0conngrumgrv2  27599  vdgn1frgrv2  27704  imadifxp  29977  acunirnmpt  30024  fnpreimac  30036  nn0sqeq1  30078  xaddeq0  30083  madjusmdetlem2  30492  xrge0iifhom  30581  signswn0  31237  signsvtn0  31247  signsvtn0OLD  31248  signstfvneq0  31250  repr0  31291  derangenlem  31752  subfacp1lem3  31763  subfacp1lem5  31765  wsuclem  32359  noseponlem  32406  ivthALT  32918  neibastop1  32942  finxpreclem2  33822  finxpreclem6  33828  tan2h  34026  poimirlem9  34044  heicant  34070  itg2addnclem2  34087  lsatfixedN  35163  islshpat  35171  lkrshp  35259  2llnm3N  35723  dalemdnee  35820  cdleme18b  36446  cdleme40m  36621  cdlemg12g  36803  cdlemh  36971  cdlemj3  36977  tendoconid  36983  cdlemk3  36987  cdlemk12  37004  cdlemk12u  37026  cdlemk46  37102  cdlemk54  37112  erngdvlem4  37145  erngdvlem4-rN  37153  dibn0  37307  dihglblem2aN  37447  dochshpncl  37538  dochsnnz  37604  dochsatshpb  37606  lcfl7lem  37653  lcfl8b  37658  lcfrlem33  37729  lcfr  37739  hdmaprnlem3uN  38005  nn0rppwr  38162  cmpfiiin  38220  pell1234qrne0  38377  rmxyneg  38444  fnwe2lem2  38580  kelac1  38592  wnefimgd  39416  radcnvrat  39469  binomcxplemfrat  39506  binomcxplemradcnv  39507  disjrnmpt2  40298  disjf1o  40301  choicefi  40313  ioondisj2  40626  ioondisj1  40627  lptioo2  40771  lptioo1  40772  0ellimcdiv  40789  liminflbuz2  40955  ioodvbdlimc1  41076  ioodvbdlimc2  41078  stoweidlem31  41175  stoweidlem59  41203  wallispilem4  41212  wallispi  41214  stirlinglem3  41220  stirlinglem14  41231  dirkerper  41240  dirkertrigeq  41245  dirkercncflem2  41248  fourierdlem4  41255  fourierdlem30  41281  fourierdlem41  41292  fourierdlem42  41293  fourierdlem44  41295  fourierdlem46  41296  fourierdlem48  41298  fourierdlem49  41299  fourierdlem62  41312  fourierdlem74  41324  fourierdlem75  41325  fourierdlem79  41329  fourierdlem102  41352  fourierdlem114  41364  fouriersw  41375  elaa2lem  41377  elaa2  41378  etransclem24  41402  etransclem44  41422  etransclem47  41425  ioorrnopnlem  41448  subsaliuncl  41500  sge0cl  41522  meadjun  41603  meadjiunlem  41606  hoicvr  41689  ovnsubadd2lem  41786  smflimlem6  41911  smfpimcc  41941  smflimsuplem2  41954  lswn0  42412  sprvalpwn0  42422  fmtnoprmfac1lem  42497  el0ldep  43270  islindeps2  43287  ldepsnlinclem1  43309  ldepsnlinclem2  43310  itscnhlinecirc02plem1  43518