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

Theorem eqnetrd 3080
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 3072 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
41, 3mpbird 258 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wne 3013
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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  eqnetrrd  3081  3netr4d  3090  opnz  5356  xpdifid  6018  undefne0  7934  onoviun  7969  intrnfi  8868  cantnfp1lem2  9130  cantnfp1lem3  9131  wemapwe  9148  acndom2  9468  fin23lem14  9743  fin23lem40  9761  isf32lem6  9768  isf34lem5  9788  isf34lem7  9789  isf34lem6  9790  axcc2lem  9846  xaddnemnf  12617  xaddnepnf  12618  fseqsupcl  13333  hashprg  13744  elprchashprn2  13745  hash1n0  13770  limsupgre  14826  isercolllem3  15011  prodfn0  15238  ntrivcvgtail  15244  fproddiv  15303  fprodn0  15321  tanval3  15475  tanneg  15489  ruclem11  15581  bezoutr1  15901  phibndlem  16095  dfphi2  16099  0ram  16344  0ram2  16345  ram0  16346  0ramcl  16347  gsumval2  17884  sgrp2nmndlem5  18032  issubg2  18232  ghmrn  18309  pmtrmvd  18513  gsumval3  18956  pgpfaclem2  19133  ablfaclem2  19137  ablfaclem3  19138  fincygsubgodd  19163  subdrgint  19511  abvdom  19538  lbsextlem2  19860  gzrngunit  20539  zringunit  20563  cnmsgnsubg  20649  frlmssuvc2  20867  iinopn  21438  cnconn  21958  1stcfb  21981  dissnlocfin  22065  fbasrn  22420  fclscmpi  22565  alexsublem  22580  ustuqtop5  22781  cnextucn  22839  dscmet  23109  reperflem  23353  evth  23490  cmetcaulem  23818  iscmet3  23823  metsscmetcld  23845  cmetss  23846  bcthlem5  23858  bcth2  23860  mbflimsup  24194  itg1addlem4  24227  itg1climres  24242  itg2monolem1  24278  itg2i1fseq2  24284  tdeglem4  24581  deg1add  24624  deg1mul2  24635  deg1tm  24639  dgreq  24761  dgradd2  24785  dgrmul  24787  dgrmulc  24788  dgrcolem1  24790  plyrem  24821  facth  24822  fta1lem  24823  vieta1lem1  24826  vieta1lem2  24827  vieta1  24828  qaa  24839  aareccl  24842  geolim3  24855  aaliou3lem9  24866  coseq00topi  25015  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  25573  ftalem7  25583  basellem2  25586  basellem4  25588  basellem5  25589  isppw  25618  dchrptlem2  25768  lgsne0  25838  2sqlem8a  25928  2sqlem8  25929  tglnpt2  26354  midexlem  26405  colperpexlem3  26445  mideulem2  26447  lnopp2hpgb  26476  subgruhgredgd  26993  wwlksnext  27598  wspthsnonn0vne  27623  clwwisshclwws  27720  vdn0conngrumgrv2  27902  vdgn1frgrv2  28002  imadifxp  30279  acunirnmpt  30332  fnpreimac  30344  xaddeq0  30403  pmtrcnelor  30662  qsidomlem2  30883  madjusmdetlem2  30992  xrge0iifhom  31079  signswn0  31729  signsvtn0  31739  signstfvneq0  31741  repr0  31781  derangenlem  32315  subfacp1lem3  32326  subfacp1lem5  32328  wsuclem  33009  noseponlem  33068  ivthALT  33580  neibastop1  33604  finxpreclem2  34553  finxpreclem6  34559  tan2h  34765  poimirlem9  34782  heicant  34808  itg2addnclem2  34825  lsatfixedN  36025  islshpat  36033  lkrshp  36121  2llnm3N  36585  dalemdnee  36682  cdleme18b  37308  cdleme40m  37483  cdlemg12g  37665  cdlemh  37833  cdlemj3  37839  tendoconid  37845  cdlemk3  37849  cdlemk12  37866  cdlemk12u  37888  cdlemk46  37964  cdlemk54  37974  erngdvlem4  38007  erngdvlem4-rN  38015  dibn0  38169  dihglblem2aN  38309  dochshpncl  38400  dochsnnz  38466  dochsatshpb  38468  lcfl7lem  38515  lcfl8b  38520  lcfrlem33  38591  lcfr  38601  hdmaprnlem3uN  38867  nn0rppwr  39060  remul01  39115  remulinvcom  39126  3cubeslem2  39160  cmpfiiin  39172  pell1234qrne0  39328  rmxyneg  39395  fnwe2lem2  39529  kelac1  39541  wnefimgd  40390  radcnvrat  40523  binomcxplemfrat  40560  binomcxplemradcnv  40561  disjrnmpt2  41325  disjf1o  41328  choicefi  41339  ioondisj2  41643  ioondisj1  41644  lptioo2  41788  lptioo1  41789  0ellimcdiv  41806  liminflbuz2  41972  ioodvbdlimc1  42094  ioodvbdlimc2  42096  stoweidlem31  42193  stoweidlem59  42221  wallispilem4  42230  wallispi  42232  stirlinglem3  42238  stirlinglem14  42249  dirkerper  42258  dirkertrigeq  42263  dirkercncflem2  42266  fourierdlem4  42273  fourierdlem30  42299  fourierdlem41  42310  fourierdlem42  42311  fourierdlem44  42313  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem62  42330  fourierdlem74  42342  fourierdlem75  42343  fourierdlem79  42347  fourierdlem102  42370  fourierdlem114  42382  fouriersw  42393  elaa2lem  42395  elaa2  42396  etransclem24  42420  etransclem44  42440  etransclem47  42443  ioorrnopnlem  42466  subsaliuncl  42518  sge0cl  42540  meadjun  42621  meadjiunlem  42624  hoicvr  42707  ovnsubadd2lem  42804  smflimlem6  42929  smfpimcc  42959  smflimsuplem2  42972  lswn0  43481  sprvalpwn0  43522  fmtnoprmfac1lem  43603  el0ldep  44449  islindeps2  44466  ldepsnlinclem1  44488  ldepsnlinclem2  44489  itscnhlinecirc02plem1  44697
  Copyright terms: Public domain W3C validator