MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr4i Unicode version

Theorem eqtr4i 2389
Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqtr4i.1  |-  A  =  B
eqtr4i.2  |-  C  =  B
Assertion
Ref Expression
eqtr4i  |-  A  =  C

Proof of Theorem eqtr4i
StepHypRef Expression
1 eqtr4i.1 . 2  |-  A  =  B
2 eqtr4i.2 . . 3  |-  C  =  B
32eqcomi 2370 . 2  |-  B  =  C
41, 3eqtri 2386 1  |-  A  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1647
This theorem is referenced by:  3eqtr2i  2392  3eqtr2ri  2393  3eqtr4i  2396  3eqtr4ri  2397  rabab  2890  cbvralcsf  3229  cbvrabcsf  3232  dfin5  3246  dfdif2  3247  uneqin  3508  unrab  3527  inrab  3528  inrab2  3529  difrab  3530  dfrab3ss  3534  rabun2  3535  rabxm  3565  difidALT  3612  difdifdir  3630  dfif3  3664  dfif5  3666  tpidm  3823  ssunpr  3876  sstp  3878  dfint2  3966  iunrab  4051  uniiun  4057  intiin  4058  0iin  4062  mptv  4214  dfepfr  4481  epfrc  4482  xpundi  4844  xpundir  4845  resiundiOLD  4848  resiun2  5078  resopab  5099  opabresid  5106  dffr3  5148  dfse2  5149  cnvun  5189  imaundir  5197  imainrect  5222  cnvcnv2  5230  cnvcnvres  5239  dmtpop  5252  rnsnopg  5255  rnco2  5283  dmco  5284  co01  5290  unidmrn  5305  dfdm2  5307  dfmpt3  5471  mptun  5479  funcocnv2  5604  dffv2  5699  fnasrn  5813  fpr  5815  fmptap  5823  abrexex2g  5888  abrexex2  5901  dmoprab  6054  rnoprab2  6057  mpt2v  6063  mpt2mptx  6064  1stval2  6264  2ndval2  6265  fo1st  6266  fo2nd  6267  xp2  6284  dfoprab4f  6305  fmpt2co  6330  tposmpt2  6413  riotav  6451  cbvriota  6457  recsfval  6539  rdgsucmpt2  6585  frsucmpt2  6594  df2o3  6634  o1p1e2  6681  oarec  6702  omopthlem2  6796  ecqs  6865  qliftf  6889  erovlem  6897  mapsnf1o3  6959  ixp0x  6987  omf1o  7108  xpf1o  7166  mapunen  7173  enp1ilem  7239  pwfi  7298  marypha1lem  7333  marypha2lem4  7338  dfoi  7373  infeq5i  7484  oemapso  7531  cantnflem1  7538  rankelop  7693  leweon  7786  r0weon  7787  kmlem11  7933  infcda1  7966  ackbij1lem16  8008  cf0  8024  cfsmolem  8043  alephsuc3  8349  fpwwe  8415  canthp1lem1  8421  wuncval2  8516  prlem936  8818  m1p1sr  8861  m1m1sr  8862  dfcnqs  8911  ssxr  9039  mul02lem2  9136  addid1  9139  3m1e2  9989  3m1e2OLD  9990  2p2e4  9991  3p2e5  10004  3p3e6  10005  4p2e6  10006  4p3e7  10007  4p4e8  10008  5p2e7  10009  5p3e8  10010  5p4e9  10011  5p5e10  10012  6p2e8  10013  6p3e9  10014  6p4e10  10015  7p2e9  10016  7p3e10  10017  8p2e10  10018  nn0supp  10166  nnzrab  10202  nn0zrab  10203  dec0u  10290  dec0h  10291  decsuc  10298  decsucc  10302  numma  10306  decma  10313  decmac  10314  decma2c  10315  decadd  10316  decaddc  10317  decmul1c  10322  decmul2c  10323  5t5e25  10351  6t6e36  10356  8t6e48  10367  nn0uz  10413  nnuz  10414  xaddcom  10717  x2times  10771  ioomax  10877  iccmax  10878  ioopos  10879  ioorp  10880  prunioo  10917  fseq1p1m1  11012  fzo0to2pr  11071  fzo0to3tp  11072  om2uzrdg  11183  fzennn  11194  irec  11367  binom2aiOLD  11378  facnn  11455  fac0  11456  faclbnd2  11469  faclbnd4lem1  11471  hashfun  11587  hashbclem  11588  hashf1lem1  11591  hashf1lem2  11592  fz1isolem  11597  s1co  11689  fsumrev2  12452  fsumparts  12472  fsumiun  12487  isumnn0nn  12509  harmonic  12525  0.999...  12545  ege2le3  12579  cos1bnd  12675  efieq1re  12687  eirrlem  12690  qnnen  12700  cpnnen  12715  ruclem6  12721  3dvds  12799  m1bits  12839  algrp1  12952  phiprmpw  13052  prmreclem4  13174  4sqlem11  13210  4sqlem19  13218  dec5dvds  13287  decsplit1  13305  5prm  13318  7prm  13320  1259lem2  13338  1259lem3  13339  1259lem4  13340  1259lem5  13341  1259prm  13342  2503lem1  13343  2503lem2  13344  2503lem3  13345  2503prm  13346  4001lem1  13347  4001lem2  13348  4001lem3  13349  4001lem4  13350  4001prm  13351  ndxid  13377  strle1  13447  grpbasex  13459  grpplusgx  13460  divslem  13655  xpslem  13685  acsfn1  13773  acsfn2  13775  comfffval2  13814  oppchomf  13833  xpchomfval  14163  xpccofval  14166  1stfval  14175  2ndfval  14178  oduleg  14446  grpinvfvi  14733  gaorb  14971  symgbas  14982  symgga  14996  cayleylem1  14997  cntri  15016  cntrsubgnsg  15026  cntrnsg  15027  oppglem  15033  oppgcntr  15048  gsumwrev  15049  efgval2  15243  efgredlemc  15264  efgcpbllema  15273  frgpnabllem1  15371  gsumzaddlem  15413  mgplem  15540  opprlem  15620  oppr0  15625  opprneg  15627  rlmscaf  16170  mplbas  16384  mpladd  16396  mplmul  16397  mplvsca2  16400  ressmplbas2  16409  ltbwe  16424  evlslem4  16455  psr1bas2  16479  ply1bas  16484  ply1assa  16488  mplplusg  16507  mplvscafvalOLD  16508  mplmulr  16509  psr1plusg  16510  psr1vsca  16511  psr1mulr  16512  ply1plusg  16513  ply1vsca  16514  ply1mulr  16515  ply1mpl0  16543  ply1mpl1  16544  coe1mul  16557  xrsds  16631  zrngunit  16655  gsumfsum  16656  ocv0  16794  thlle  16814  thlleval  16815  indistpsx  16964  iuncld  16999  tgrest  17107  resstopn  17133  leordtval2  17159  xkouni  17511  ptclsg  17526  ptuncnv  17715  ptunhmeo  17716  alexsubALTlem4  17957  tsmsf1o  18040  ressxms  18284  uniretop  18484  cnfldtopn  18504  xrtgioo  18525  zcld  18532  icccmp  18544  xrge0gsumle  18552  xrge0tsms  18553  metnrmlem3  18579  fsum2cn  18589  cnmpt2pc  18641  oprpiece1res1  18664  oprpiece1res2  18665  evth  18672  evth2  18673  om1opn  18749  pi1xfrf  18766  pi1xfrcnv  18770  pi1cof  18772  clsocv  18892  cncmet  18959  ismbl  19100  shftmbl  19111  ioorinv  19146  itg1addlem4  19269  itg2cnlem1  19331  iblitg  19338  itg0  19349  itgss3  19384  ditgneg  19422  limcdif  19441  limciun  19459  dvexp  19517  dvef  19542  dvcnvrelem2  19580  ftc1  19604  plyremlem  19899  aannenlem2  19924  taylply2  19962  dvradcnv  20015  pserdvlem2  20022  reefgim  20044  cospi  20058  sincos6thpi  20101  tanregt0  20119  dflog2  20136  logfac  20173  dvlog  20220  cxpexp  20237  cxpmul2  20258  cxpsqr  20272  dvsqr  20306  cxpcn2  20308  ang180lem2  20330  isosctrlem2  20341  1cubrlem  20359  1cubr  20360  quart1lem  20373  atancj  20428  atanlogaddlem  20431  atansopn  20450  leibpilem2  20459  log2cnv  20462  log2ublem3  20466  birthdaylem1  20468  birthdaylem2  20469  birthday  20471  dfarea  20477  wilthlem2  20530  ftalem3  20535  ftalem7  20539  basellem2  20542  ppiprm  20612  ppinprm  20613  chtprm  20614  chtnprm  20615  ppi2  20631  ppi3  20632  ppiub  20666  chtub  20674  bclbnd  20742  bposlem8  20753  lgsdilem  20784  lgsdir2lem1  20785  lgsdir2lem2  20786  lgsdir2lem3  20787  lgsquadlem2  20817  lgsquad2lem2  20821  rplogsum  20899  mulog2sumlem2  20907  pnt2  20985  usgrares1  21094  ex-pw  21127  ex-xp  21134  ex-rn  21138  ablosn  21325  efghgrp  21351  nvvop  21478  nvm  21512  cnims  21579  ip0i  21716  ip1ilem  21717  ipdirilem  21720  ipasslem10  21730  h2hva  21867  h2hsm  21868  h2hvs  21870  axhfvadd-zf  21875  axhvcom-zf  21876  axhvass-zf  21877  axhv0cl-zf  21878  axhvaddid-zf  21879  axhfvmul-zf  21880  axhvmulid-zf  21881  axhvmulass-zf  21882  axhvdistr1-zf  21883  axhvdistr2-zf  21884  axhvmul0-zf  21885  axhfi-zf  21886  axhis1-zf  21887  axhis2-zf  21888  axhis3-zf  21889  axhis4-zf  21890  axhcompl-zf  21891  normlem0  22001  normlem1  22002  normlem2  22003  normlem4  22005  normlem9  22010  bcseqi  22012  dfhnorm2  22014  norm3difi  22039  normpari  22046  normpar2i  22048  polid2i  22049  polidi  22050  hhba  22059  hhims  22064  hhims2  22065  hhsssh  22159  hhssims  22165  hhssims2  22166  shsval3i  22280  dfch2  22299  cmcm2i  22485  fh2  22511  qlaxr3i  22528  spansnji  22538  pjcji  22576  ho0val  22643  df0op2  22645  hosd1i  22715  hosd2i  22716  eigorthi  22730  hhlnoi  22793  hhnmoi  22794  hhbloi  22795  bra0  22843  nmop0  22879  nmfn0  22880  lnopeq0lem1  22898  lnopunilem1  22903  lnophmlem2  22910  nmopcoadji  22994  pjhmopidm  23076  cvmdi  23217  cdj3lem3  23331  cdj3lem3b  23333  abrexdomjm  23383  iundifdifd  23410  iundifdif  23411  df1stres  23494  df2ndres  23495  xrge0tsmsd  23614  tpr2rico  23665  xrge0mulc1cn  23682  lmxrge0  23692  ucnimalem  23774  cnflduss  23815  esumpfinvallem  23929  esumcocn  23935  hasheuni  23940  esumcvg  23941  measinblem  24037  aean  24058  sxbrsigalem3  24085  dya2iocival  24086  dya2iocucvr  24097  sxbrsigalem1  24098  sxbrsigalem2  24099  sxbrsigalem5  24101  sxbrsiga  24103  coinfliplem  24184  coinflipprob  24185  ballotlemfval  24195  ballotth  24243  lgamgulmlem5  24265  lgambdd  24269  derang0  24303  subfacp1lem1  24313  subfacp1lem6  24319  kur14lem7  24346  cvmsss2  24408  cvmliftlem8  24426  cvmliftlem10  24428  eupath2lem3  24490  konigsberg  24498  ghomgrpilem2  24580  faclim  24840  predidm  24929  tz6.26  24946  dftrpred2  24963  bdayfo  25070  pprodcnveq  25164  dfon4  25174  fobigcup  25181  dfiota3  25203  dfrdg4  25230  axsegconlem9  25295  ax5seglem7  25305  axlowdimlem16  25327  bpoly2  25534  bpoly3  25535  bpoly4  25536  rankeq1o  25543  ssoninhaus  25629  onint1  25630  rabiun2  25667  refssfne  25801  fnopabco  25895  abrexdom  25912  cncfres  25991  mapfzcons  26299  eldioph4b  26400  diophren  26402  rabren3dioph  26404  pwssplit4  26697  dsmmval2  26708  pwfi2f1o  26766  frlmpwfi  26768  psgnunilem2  26924  cnmsgngrp  26942  mendplusgfval  26999  mendmulrfval  27001  mendvscafval  27004  idomodle  27018  cytpval  27034  lhe4.4ex1a  27052  compne  27148  refsum2cnlem1  27214  stoweidlem13  27268  stoweidlem32  27287  stoweidlem62  27317  wallispilem4  27323  wallispi2lem1  27326  wallispi2lem2  27327  wallispi2  27328  stirlinglem3  27331  cusgrares  27637  bnj1400  28632  bnj66  28656  bnj882  28722  cdleme3d  30491  cdleme7a  30503  cdleme31sdnN  30647  cdlemk45  31207
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator