MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqnetrd Structured version   Visualization version   GIF version

Theorem eqnetrd 2890
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
StepHypRef Expression
1 eqnetrd.2 . 2 (𝜑𝐵𝐶)
2 eqnetrd.1 . . 3 (𝜑𝐴 = 𝐵)
32neeq1d 2882 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 247 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  eqnetrrd  2891  3netr4d  2900  opnz  4971  xpdifid  5597  undefne0  7450  onoviun  7485  intrnfi  8363  cantnfp1lem2  8614  cantnfp1lem3  8615  wemapwe  8632  acndom2  8915  fin23lem14  9193  fin23lem40  9211  isf32lem6  9218  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  axcc2lem  9296  xaddnemnf  12105  xaddnepnf  12106  fseqsupcl  12816  hashprg  13220  hashprgOLD  13221  elprchashprn2  13222  hash1n0  13247  limsupgre  14256  isercolllem3  14441  prodfn0  14670  ntrivcvgtail  14676  fproddiv  14735  fprodn0  14753  tanval3  14908  tanneg  14922  ruclem11  15013  bezoutr1  15329  phibndlem  15522  dfphi2  15526  0ram  15771  0ram2  15772  ram0  15773  0ramcl  15774  gsumval2  17327  sgrp2nmndlem5  17463  issubg2  17656  ghmrn  17720  pmtrmvd  17922  gsumval3  18354  pgpfaclem2  18527  ablfaclem2  18531  ablfaclem3  18532  abvdom  18886  lbsextlem2  19207  gzrngunit  19860  zringunit  19884  cnmsgnsubg  19971  frlmssuvc2  20182  iinopn  20755  cnconn  21273  1stcfb  21296  dissnlocfin  21380  fbasrn  21735  fclscmpi  21880  alexsublem  21895  ustuqtop5  22096  cnextucn  22154  dscmet  22424  reperflem  22668  evth  22805  cmetcaulem  23132  iscmet3  23137  cmetss  23159  bcthlem5  23171  bcth2  23173  mbflimsup  23478  itg1addlem4  23511  itg1climres  23526  itg2monolem1  23562  itg2i1fseq2  23568  tdeglem4  23865  deg1add  23908  deg1mul2  23919  deg1tm  23923  dgreq  24045  dgradd2  24069  dgrmul  24071  dgrmulc  24072  dgrcolem1  24074  plyrem  24105  facth  24106  fta1lem  24107  vieta1lem1  24110  vieta1lem2  24111  vieta1  24112  qaa  24123  aareccl  24126  geolim3  24139  aaliou3lem9  24150  coseq00topi  24299  cosne0  24321  tanord  24329  tanarg  24410  cxpne0  24468  cxpsqrt  24494  logbrec  24565  chordthmlem  24604  chordthmlem2  24605  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  quartlem4  24632  atandmneg  24678  atandmcj  24681  atancj  24682  atanrecl  24683  atanlogsublem  24687  efiatan2  24689  tanatan  24691  atandmtan  24692  cosatan  24693  cosatanne0  24694  wilthlem2  24840  ftalem7  24850  basellem2  24853  basellem4  24855  basellem5  24856  isppw  24885  dchrptlem2  25035  lgsne0  25105  2sqlem8a  25195  2sqlem8  25196  tglnpt2  25581  midexlem  25632  colperpexlem3  25669  mideulem2  25671  lnopp2hpgb  25700  subgruhgredgd  26221  wwlksnext  26856  wspthsnonn0vne  26882  clwwisshclwws  26972  vdn0conngrumgrv2  27174  vdgn1frgrv2  27276  imadifxp  29540  acunirnmpt  29587  nn0sqeq1  29641  xaddeq0  29646  madjusmdetlem2  30022  xrge0iifhom  30111  signswn0  30765  signsvtn0  30775  signstfvneq0  30777  repr0  30817  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  wsuclem  31895  noseponlem  31942  ivthALT  32455  neibastop1  32479  finxpreclem2  33357  finxpreclem6  33363  tan2h  33531  poimirlem9  33548  heicant  33574  itg2addnclem2  33592  lsatfixedN  34614  islshpat  34622  lkrshp  34710  2llnm3N  35173  dalemdnee  35270  cdleme18b  35897  cdleme40m  36072  cdlemg12g  36254  cdlemh  36422  cdlemj3  36428  tendoconid  36434  cdlemk3  36438  cdlemk12  36455  cdlemk12u  36477  cdlemk46  36553  cdlemk54  36563  erngdvlem4  36596  erngdvlem4-rN  36604  dibn0  36759  dihglblem2aN  36899  dochshpncl  36990  dochsnnz  37056  dochsatshpb  37058  lcfl7lem  37105  lcfl8b  37110  lcfrlem33  37181  lcfr  37191  hdmaprnlem3uN  37460  cmpfiiin  37577  pell1234qrne0  37734  rmxyneg  37802  fnwe2lem2  37938  kelac1  37950  wnefimgd  38777  radcnvrat  38830  binomcxplemfrat  38867  binomcxplemradcnv  38868  disjrnmpt2  39689  disjf1o  39692  choicefi  39706  ioondisj2  40032  ioondisj1  40033  lptioo2  40181  lptioo1  40182  0ellimcdiv  40199  ioodvbdlimc1  40466  ioodvbdlimc2  40468  stoweidlem31  40566  stoweidlem59  40594  wallispilem4  40603  wallispi  40605  stirlinglem3  40611  stirlinglem14  40622  dirkerper  40631  dirkertrigeq  40636  dirkercncflem2  40639  fourierdlem4  40646  fourierdlem30  40672  fourierdlem41  40683  fourierdlem42  40684  fourierdlem44  40686  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem62  40703  fourierdlem74  40715  fourierdlem75  40716  fourierdlem79  40720  fourierdlem102  40743  fourierdlem114  40755  fouriersw  40766  elaa2lem  40768  elaa2  40769  etransclem24  40793  etransclem44  40813  etransclem47  40816  ioorrnopnlem  40842  subsaliuncl  40894  sge0cl  40916  meadjun  40997  meadjiunlem  41000  hoicvr  41083  ovnsubadd2lem  41180  smflimlem6  41305  smfpimcc  41335  smflimsuplem2  41348  lswn0  41705  pfxn0  41719  fmtnoprmfac1lem  41801  sprvalpwn0  42058  el0ldep  42580  islindeps2  42597  ldepsnlinclem1  42619  ldepsnlinclem2  42620
  Copyright terms: Public domain W3C validator