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

Theorem eqnetrd 3083
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 3075 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 258 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  eqnetrrd  3084  3netr4d  3093  opnz  5357  xpdifid  6019  undefne0  7936  onoviun  7971  intrnfi  8869  cantnfp1lem2  9131  cantnfp1lem3  9132  wemapwe  9149  acndom2  9469  fin23lem14  9744  fin23lem40  9762  isf32lem6  9769  isf34lem5  9789  isf34lem7  9790  isf34lem6  9791  axcc2lem  9847  xaddnemnf  12619  xaddnepnf  12620  fseqsupcl  13335  hashprg  13746  elprchashprn2  13747  hash1n0  13772  limsupgre  14828  isercolllem3  15013  prodfn0  15240  ntrivcvgtail  15246  fproddiv  15305  fprodn0  15323  tanval3  15477  tanneg  15491  ruclem11  15583  bezoutr1  15903  phibndlem  16097  dfphi2  16101  0ram  16346  0ram2  16347  ram0  16348  0ramcl  16349  gsumval2  17886  sgrp2nmndlem5  18034  issubg2  18234  ghmrn  18311  pmtrmvd  18515  gsumval3  18958  pgpfaclem2  19135  ablfaclem2  19139  ablfaclem3  19140  fincygsubgodd  19165  subdrgint  19513  abvdom  19540  lbsextlem2  19862  gzrngunit  20541  zringunit  20565  cnmsgnsubg  20651  frlmssuvc2  20869  iinopn  21440  cnconn  21960  1stcfb  21983  dissnlocfin  22067  fbasrn  22422  fclscmpi  22567  alexsublem  22582  ustuqtop5  22783  cnextucn  22841  dscmet  23111  reperflem  23355  evth  23492  cmetcaulem  23820  iscmet3  23825  metsscmetcld  23847  cmetss  23848  bcthlem5  23860  bcth2  23862  mbflimsup  24196  itg1addlem4  24229  itg1climres  24244  itg2monolem1  24280  itg2i1fseq2  24286  tdeglem4  24583  deg1add  24626  deg1mul2  24637  deg1tm  24641  dgreq  24763  dgradd2  24787  dgrmul  24789  dgrmulc  24790  dgrcolem1  24792  plyrem  24823  facth  24824  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  vieta1  24830  qaa  24841  aareccl  24844  geolim3  24857  aaliou3lem9  24868  coseq00topi  25017  cosne0  25041  tanord  25049  tanarg  25129  cxpne0  25187  cxpsqrt  25213  logbrec  25287  chordthmlem  25337  chordthmlem2  25338  dcubic  25351  mcubic  25352  cubic2  25353  cubic  25354  quartlem4  25365  atandmneg  25411  atandmcj  25414  atancj  25415  atanrecl  25416  atanlogsublem  25420  efiatan2  25422  tanatan  25424  atandmtan  25425  cosatan  25426  cosatanne0  25427  wilthlem2  25574  ftalem7  25584  basellem2  25587  basellem4  25589  basellem5  25590  isppw  25619  dchrptlem2  25769  lgsne0  25839  2sqlem8a  25929  2sqlem8  25930  tglnpt2  26355  midexlem  26406  colperpexlem3  26446  mideulem2  26448  lnopp2hpgb  26477  subgruhgredgd  26994  wwlksnext  27599  wspthsnonn0vne  27624  clwwisshclwws  27721  vdn0conngrumgrv2  27903  vdgn1frgrv2  28003  imadifxp  30280  acunirnmpt  30333  fnpreimac  30345  xaddeq0  30404  pmtrcnelor  30663  qsidomlem2  30884  madjusmdetlem2  30993  xrge0iifhom  31080  signswn0  31730  signsvtn0  31740  signstfvneq0  31742  repr0  31782  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  wsuclem  33010  noseponlem  33069  ivthALT  33581  neibastop1  33605  finxpreclem2  34554  finxpreclem6  34560  tan2h  34766  poimirlem9  34783  heicant  34809  itg2addnclem2  34826  lsatfixedN  36027  islshpat  36035  lkrshp  36123  2llnm3N  36587  dalemdnee  36684  cdleme18b  37310  cdleme40m  37485  cdlemg12g  37667  cdlemh  37835  cdlemj3  37841  tendoconid  37847  cdlemk3  37851  cdlemk12  37868  cdlemk12u  37890  cdlemk46  37966  cdlemk54  37976  erngdvlem4  38009  erngdvlem4-rN  38017  dibn0  38171  dihglblem2aN  38311  dochshpncl  38402  dochsnnz  38468  dochsatshpb  38470  lcfl7lem  38517  lcfl8b  38522  lcfrlem33  38593  lcfr  38603  hdmaprnlem3uN  38869  nn0rppwr  39062  remul01  39117  remulinvcom  39128  3cubeslem2  39162  cmpfiiin  39174  pell1234qrne0  39330  rmxyneg  39397  fnwe2lem2  39531  kelac1  39543  wnefimgd  40392  radcnvrat  40526  binomcxplemfrat  40563  binomcxplemradcnv  40564  disjrnmpt2  41329  disjf1o  41332  choicefi  41343  ioondisj2  41647  ioondisj1  41648  lptioo2  41792  lptioo1  41793  0ellimcdiv  41810  liminflbuz2  41976  ioodvbdlimc1  42098  ioodvbdlimc2  42100  stoweidlem31  42197  stoweidlem59  42225  wallispilem4  42234  wallispi  42236  stirlinglem3  42242  stirlinglem14  42253  dirkerper  42262  dirkertrigeq  42267  dirkercncflem2  42270  fourierdlem4  42277  fourierdlem30  42303  fourierdlem41  42314  fourierdlem42  42315  fourierdlem44  42317  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem62  42334  fourierdlem74  42346  fourierdlem75  42347  fourierdlem79  42351  fourierdlem102  42374  fourierdlem114  42386  fouriersw  42397  elaa2lem  42399  elaa2  42400  etransclem24  42424  etransclem44  42444  etransclem47  42447  ioorrnopnlem  42470  subsaliuncl  42522  sge0cl  42544  meadjun  42625  meadjiunlem  42628  hoicvr  42711  ovnsubadd2lem  42808  smflimlem6  42933  smfpimcc  42963  smflimsuplem2  42976  lswn0  43451  sprvalpwn0  43492  fmtnoprmfac1lem  43573  el0ldep  44419  islindeps2  44436  ldepsnlinclem1  44458  ldepsnlinclem2  44459  itscnhlinecirc02plem1  44667
  Copyright terms: Public domain W3C validator