Theorem eqnetrd 3022

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  eqnetrrd  3023  3netr4d  3032  opnz  5449  xpdifid  6160  undefne0  8278  onoviun  8332  intrnfi  9386  cantnfp1lem2  9658  cantnfp1lem3  9659  wemapwe  9676  acndom2  10057  fin23lem14  10335  fin23lem40  10353  isf32lem6  10360  isf34lem5  10380  isf34lem7  10381  isf34lem6  10382  axcc2lem  10438  xaddnemnf  13288  xaddnepnf  13289  fseqsupcl  14041  hashprg  14459  elprchashprn2  14460  hash1n0  14486  limsupgre  15568  isercolllem3  15754  prodfn0  15983  ntrivcvgtail  15989  fproddiv  16048  fprodn0  16066  tanval3  16222  tanneg  16236  ruclem11  16328  nn0rppwr  16651  bezoutr1  16659  phibndlem  16861  dfphi2  16865  0ram  17112  0ram2  17113  ram0  17114  0ramcl  17115  gsumval2  18788  sgrp2nmndlem5  19041  issubg2  19265  ghmrn  19356  pmtrmvd  19583  gsumval3  20034  pgpfaclem2  20211  ablfaclem2  20215  ablfaclem3  20216  fincygsubgodd  20241  subdrgint  20969  abvdom  20996  lbsextlem2  21346  qsidomlem2  21544  cndrng  21614  gzrngunit  21646  zringunit  21679  cnmsgnsubg  21790  frlmssuvc2  22008  mhpmulcl  22377  iinopn  23127  cnconn  23647  1stcfb  23670  dissnlocfin  23755  fbasrn  24110  fclscmpi  24255  alexsublem  24270  ustuqtop5  24471  cnextucn  24528  dscmet  24798  reperflem  25045  evth  25187  cmetcaulem  25516  iscmet3  25521  metsscmetcld  25543  cmetss  25544  bcthlem5  25556  bcth2  25558  mbflimsup  25894  itg1addlem4  25927  itg1climres  25942  itg2monolem1  25978  itg2i1fseq2  25984  tdeglem4  26285  deg1add  26328  deg1mul2  26339  deg1tm  26344  dgreq  26470  dgradd2  26494  dgrmul  26496  dgrmulc  26497  dgrcolem1  26499  plyrem  26535  facth  26536  fta1lem  26537  vieta1lem1  26542  vieta1lem2  26543  vieta1  26544  qaa  26556  aareccl  26562  geolim3  26575  aaliou3lem9  26586  coseq00topi  26740  cosne0  26766  tanord  26775  tanarg  26856  cxpne0  26914  cxpsqrt  26940  logbrec  27019  chordthmlem  27069  chordthmlem2  27070  dcubic  27083  mcubic  27084  cubic2  27085  cubic  27086  quartlem4  27097  atandmneg  27143  atandmcj  27146  atancj  27147  atanrecl  27148  atanlogsublem  27152  efiatan2  27154  tanatan  27156  atandmtan  27157  cosatan  27158  cosatanne0  27159  wilthlem2  27305  ftalem7  27315  basellem2  27318  basellem4  27320  basellem5  27321  isppw  27350  dchrptlem2  27501  lgsne0  27571  2sqlem8a  27661  2sqlem8  27662  noseponlem  27900  recsne0  28457  tglnpt2  29000  midexlem  29043  colperpexlem3  29087  mideulem2  29089  lnopp2hpgb  29120  angmgmaddov1  29267  subgruhgredgd  29744  wwlksnext  30361  wspthsnonn0vne  30385  clwwisshclwws  30485  vdn0conngrumgrv2  30676  vdgn1frgrv2  30776  nrt2irr  30953  ifnetrue  33022  ifnefals  33023  imadifxp  33074  acunirnmpt  33132  fnpreimac  33143  quad3d  33220  xaddeq0  33224  pmtrcnelor  33531  domnprodn0  33718  domnprodeq0  33719  drnglring  33902  dflringlem3  33906  dflring4  33908  ply1dg3rt0irred  33994  m1pmeq  33995  mplmulmvr  34049  esplyfvaln  34084  esplyind  34085  ply1annnr  34213  minplyirred  34221  rtelextdg2lem  34236  constrrtcclem  34244  constrconj  34255  constrext2chnlem  34260  constrremulcl  34277  constrrecl  34279  constrreinvcl  34282  2sqr3minply  34290  2sqr3nconstr  34291  cos9thpiminplylem1  34292  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminply  34298  cos9thpinconstrlem1  34299  cos9thpinconstrlem2  34300  cos9thpinconstr  34301  madjusmdetlem2  34338  zar0ring  34388  xrge0iifhom  34447  signswn0  35068  signsvtn0  35078  signstfvneq0  35080  repr0  35119  kard0b  35685  derangenlem  35750  subfacp1lem3  35761  subfacp1lem5  35763  wsuclem  36402  ivthALT  36954  neibastop1  36978  weiunfrlem  37083  finxpreclem2  38144  finxpreclem6  38150  tan2h  38366  poimirlem9  38378  heicant  38404  itg2addnclem2  38421  lsatfixedN  39882  islshpat  39890  lkrshp  39978  2llnm3N  40442  dalemdnee  40539  cdleme18b  41165  cdleme40m  41340  cdlemg12g  41522  cdlemh  41690  cdlemj3  41696  tendoconid  41702  cdlemk3  41706  cdlemk12  41723  cdlemk12u  41745  cdlemk46  41821  cdlemk54  41831  erngdvlem4  41864  erngdvlem4-rN  41872  dibn0  42026  dihglblem2aN  42166  dochshpncl  42257  dochsnnz  42323  dochsatshpb  42325  lcfl7lem  42372  lcfl8b  42377  lcfrlem33  42448  lcfr  42458  hdmaprnlem3uN  42724  aks4d1p1p7  42940  fldhmf1  42956  primrootspoweq0  42972  idomnnzpownz  42998  idomnnzgmulnz  42999  aks6d1c5lem2  43004  deg1gprod  43006  unitscyglem4  43064  25or6to4  43072  tanhalfpim  43224  remul01  43282  remulinvcom  43308  domnexpgn0cl  43405  ricdrng1  43410  prjcrv0  43479  3cubeslem2  43530  cmpfiiin  43542  pell1234qrne0  43694  rmxyneg  43761  fnwe2lem2  43892  kelac1  43904  wnefimgd  45001  radcnvrat  45138  binomcxplemfrat  45175  binomcxplemradcnv  45176  disjrnmpt2  46020  disjf1o  46023  choicefi  46031  ioondisj2  46323  ioondisj1  46324  lptioo2  46461  lptioo1  46462  0ellimcdiv  46477  liminflbuz2  46643  ioodvbdlimc1  46761  ioodvbdlimc2  46763  stoweidlem31  46859  stoweidlem59  46887  wallispilem4  46896  wallispi  46898  stirlinglem3  46904  stirlinglem14  46915  dirkerper  46924  dirkertrigeq  46929  dirkercncflem2  46932  fourierdlem4  46939  fourierdlem30  46965  fourierdlem41  46976  fourierdlem42  46977  fourierdlem44  46979  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem62  46996  fourierdlem74  47008  fourierdlem75  47009  fourierdlem79  47013  fourierdlem102  47036  fourierdlem114  47048  fouriersw  47059  elaa2lem  47061  elaa2  47062  etransclem24  47086  etransclem44  47106  etransclem47  47109  ioorrnopnlem  47132  subsaliuncl  47186  sge0cl  47209  meadjun  47290  meadjiunlem  47293  hoicvr  47376  ovnsubadd2lem  47473  smflimlem6  47604  smfpimcc  47636  smflimsuplem2  47649  sqrtnnaa  47731  sqrtnzqaa  47732  cjnpoly  47757  modm2nep1  48260  modm1nep2  48262  modm1p1ne  48264  lswn0  48344  sprvalpwn0  48383  fmtnoprmfac1lem  48467  grimuhgr  48803  gpg3nbgrvtx0  48992  el0ldep  49396  islindeps2  49413  ldepsnlinclem1  49435  ldepsnlinclem2  49436  itscnhlinecirc02plem1  49712  fvconstr  49790  fvconstrn0  49791  catprs  49937  fucofvalne  50251  crosspv2d  50794  crosspv3d  50795